Theorem cnvimass 6030

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 6019	. 2 ⊢ (◡𝐴 “ 𝐵) ⊆ ran ◡𝐴
2		dfdm4 5834	. 2 ⊢ dom 𝐴 = ran ◡𝐴
3	1, 2	sseqtrri 3979	1 ⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴

Syntax hints:   ⊆ wss 3897  ^◡ccnv 5613  dom cdm 5614  ran crn 5615   “ cima 5617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-xp 5620  df-cnv 5622  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627

This theorem is referenced by:  cnvimassrndm  6099  fvimacnvi  6985  elpreima  6991  cnvimainrn  7000  iinpreima  7002  rescnvimafod  7006  fconst4  7148  fsuppeq  8105  fsuppeqg  8106  pw2f1olem  8994  cnvimamptfin  9237  fisuppfi  9255  infxpenlem  9904  enfin2i  10212  fin1a2lem7  10297  smobeth  10477  fpwwe2lem3  10524  fpwwe2lem11  10532  fpwwe2lem12  10533  fpwwe2  10534  canth4  10538  canthwelem  10541  pwfseqlem4  10553  recmulnq  10855  dmrecnq  10859  ltweuz  13868  isercolllem2  15573  isercolllem3  15574  fsumss  15632  ackbijnn  15735  fprodss  15855  1arith  16839  vdwlem1  16893  vdwlem5  16897  vdwlem6  16898  vdwlem8  16900  vdwlem11  16903  ghmpreima  19150  gicer  19189  torsubg  19766  gsumzmhm  19849  gsumzoppg  19856  lmhmpreima  20982  rhmpreimaidl  21214  evpmss  21523  mplcoe5  21975  psr1baslem  22097  ofco2  22366  cnpnei  23179  cnclima  23183  iscncl  23184  cnntri  23186  cnclsi  23187  cncls2  23188  cncls  23189  cnntr  23190  cncnp  23195  cnrest2  23201  cndis  23206  2ndcomap  23373  kgencn  23471  kgencn3  23473  ptbasfi  23496  txcnmpt  23539  txdis1cn  23550  qtopval2  23611  basqtop  23626  qtopcld  23628  qtopcn  23629  qtopeu  23631  qtoprest  23632  hmeoimaf1o  23685  hmphtop  23693  hmpher  23699  ordthmeolem  23716  elfm3  23865  rnelfmlem  23867  rnelfm  23868  fmfnfmlem2  23870  fmfnfmlem4  23872  clssubg  24024  tgphaus  24032  qustgplem  24036  ucnprima  24196  ucncn  24199  xmeter  24348  imasf1oxms  24404  metustss  24466  metustexhalf  24471  metustfbas  24472  cfilucfil  24474  metuel2  24480  restmetu  24485  mbfconstlem  25555  i1fima  25606  i1fima2  25607  i1fd  25609  itg1addlem5  25628  plyeq0lem  26142  dgrcl  26165  dgrub  26166  dgrlb  26168  vieta1lem1  26245  vieta1lem2  26246  pserulm  26358  psercn2  26359  psercn2OLD  26360  psercnlem2  26361  psercnlem1  26362  psercn  26363  pserdvlem1  26364  pserdvlem2  26365  pserdv  26366  pserdv2  26367  abelth  26378  eff1olem  26484  dvlog  26587  logtayl  26596  cxpcn3lem  26684  cxpcn3  26685  resqrtcn  26686  basellem5  27022  elnlfn  31908  nlelshi  32040  xppreima  32627  ofpreima  32647  ofpreima2  32648  fnpreimac  32653  ffsrn  32711  indpreima  32846  indf1ofs  32847  pwrssmgc  32981  elrgspnsubrunlem2  33215  elrspunidl  33393  ply1degltel  33555  ply1degleel  33556  ply1degltlss  33557  esplysply  33592  dimkerim  33640  lvecendof1f1o  33646  locfinreflem  33853  zarcmplem  33894  carsggect  34331  sibfof  34353  sitgclg  34355  eulerpartlemsv2  34371  eulerpartlemsf  34372  eulerpartlemv  34377  eulerpartlemb  34381  eulerpartlemt  34384  eulerpartlemr  34387  eulerpartlemgu  34390  eulerpartlemgs2  34393  eulerpartlemn  34394  cvmliftmolem1  35325  cvmlift2lem9  35355  cvmlift3lem6  35368  cvmlift3lem7  35369  mthmsta  35622  dvtan  37709  itg2addnclem  37710  ftc1anclem6  37737  sstotbnd2  37813  keridl  38071  diaintclN  41156  dibintclN  41265  dihintcl  41442  pw2f1ocnv  43129  dnnumch3lem  43138  dnnumch3  43139  pwfi2f1o  43188  binomcxplemdvbinom  44445  binomcxplemdvsum  44447  binomcxplemnotnn0  44448  wessf1ornlem  45281  sge0f1o  46479  mbfresmf  46836  smfco  46899  smfsuplem1  46908  fcores  47166  3f1oss1  47174  uniimaprimaeqfv  47481  elsetpreimafvssdm  47485  gricrel  48018  grlicrel  48105