Theorem cnvimass 5485

Description: A preimage under any class is included in the domain of the class. (Contributed by FL, 29-Jan-2007.)

Assertion

Ref	Expression
cnvimass	⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴

Proof of Theorem cnvimass

Step	Hyp	Ref	Expression
1		imassrn 5477	. 2 ⊢ (◡𝐴 “ 𝐵) ⊆ ran ◡𝐴
2		dfdm4 5316	. 2 ⊢ dom 𝐴 = ran ◡𝐴
3	1, 2	sseqtr4i 3638	1 ⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴

Syntax hints:   ⊆ wss 3574  ^◡ccnv 5113  dom cdm 5114  ran crn 5115   “ cima 5117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-cnv 5122  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127

This theorem is referenced by:  fvimacnvi  6331  elpreima  6337  iinpreima  6345  fconst4  6478  frnsuppeq  7307  pw2f1olem  8064  cnvimamptfin  8267  fisuppfi  8283  infxpenlem  8836  enfin2i  9143  fin1a2lem7  9228  smobeth  9408  fpwwe2lem3  9455  fpwwe2lem12  9463  fpwwe2lem13  9464  fpwwe2  9465  canth4  9469  canthwelem  9472  pwfseqlem4  9484  recmulnq  9786  dmrecnq  9790  ltweuz  12760  isercolllem2  14396  isercolllem3  14397  fsumss  14456  ackbijnn  14560  fprodss  14678  1arith  15631  vdwlem1  15685  vdwlem5  15689  vdwlem6  15690  vdwlem8  15692  vdwlem11  15695  ghmpreima  17682  gicer  17718  gicerOLD  17719  torsubg  18257  gsumzmhm  18337  gsumzoppg  18344  lmhmpreima  19048  mplcoe5  19468  psr1baslem  19555  evpmss  19932  ofco2  20257  cnpnei  21068  cnclima  21072  iscncl  21073  cnntri  21075  cnclsi  21076  cncls2  21077  cncls  21078  cnntr  21079  cncnp  21084  cnrest2  21090  cndis  21095  2ndcomap  21261  kgencn  21359  kgencn3  21361  ptbasfi  21384  txcnmpt  21427  txdis1cn  21438  qtopval2  21499  basqtop  21514  qtopcld  21516  qtopcn  21517  qtopeu  21519  qtoprest  21520  hmeoimaf1o  21573  hmphtop  21581  hmpher  21587  ordthmeolem  21604  elfm3  21754  rnelfmlem  21756  rnelfm  21757  fmfnfmlem2  21759  fmfnfmlem4  21761  clssubg  21912  tgphaus  21920  qustgplem  21924  ucnprima  22086  ucncn  22089  xmeter  22238  imasf1oxms  22294  metustss  22356  metustexhalf  22361  metustfbas  22362  cfilucfil  22364  metuel2  22370  restmetu  22375  mbfconstlem  23396  i1fima  23445  i1fima2  23446  i1fd  23448  itg1addlem5  23467  plyeq0lem  23966  dgrcl  23989  dgrub  23990  dgrlb  23992  vieta1lem1  24065  vieta1lem2  24066  pserulm  24176  psercn2  24177  psercnlem2  24178  psercnlem1  24179  psercn  24180  pserdvlem1  24181  pserdvlem2  24182  pserdv  24183  pserdv2  24184  abelth  24195  eff1olem  24294  dvlog  24397  logtayl  24406  cxpcn3lem  24488  cxpcn3  24489  resqrtcn  24490  basellem5  24811  elnlfn  28787  nlelshi  28919  xppreima  29449  ofpreima  29465  ofpreima2  29466  ffsrn  29504  locfinreflem  29907  indpreima  30087  indf1ofs  30088  carsggect  30380  sibfof  30402  sitgclg  30404  eulerpartlemsv2  30420  eulerpartlemsf  30421  eulerpartlemv  30426  eulerpartlemb  30430  eulerpartlemt  30433  eulerpartlemr  30436  eulerpartlemgu  30439  eulerpartlemgs2  30442  eulerpartlemn  30443  cvmliftmolem1  31263  cvmlift2lem9  31293  cvmlift3lem6  31306  cvmlift3lem7  31307  mthmsta  31475  dvtan  33460  itg2addnclem  33461  ftc1anclem6  33490  sstotbnd2  33573  keridl  33831  diaintclN  36347  dibintclN  36456  dihintcl  36633  pw2f1ocnv  37604  dnnumch3lem  37616  dnnumch3  37617  pwfi2f1o  37666  binomcxplemdvbinom  38552  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  wessf1ornlem  39371  sge0f1o  40599  mbfresmf  40948  smfco  41009  smfsuplem1  41017