Theorem cnvimass 5626

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 5618	. 2 ⊢ (◡𝐴 “ 𝐵) ⊆ ran ◡𝐴
2		dfdm4 5454	. 2 ⊢ dom 𝐴 = ran ◡𝐴
3	1, 2	sseqtr4i 3787	1 ⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴

Syntax hints:   ⊆ wss 3723  ^◡ccnv 5248  dom cdm 5249  ran crn 5250   “ cima 5252

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-br 4787  df-opab 4847  df-xp 5255  df-cnv 5257  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262

This theorem is referenced by:  fvimacnvi  6474  elpreima  6480  iinpreima  6488  fconst4  6622  frnsuppeq  7458  pw2f1olem  8220  cnvimamptfin  8423  fisuppfi  8439  infxpenlem  9036  enfin2i  9345  fin1a2lem7  9430  smobeth  9610  fpwwe2lem3  9657  fpwwe2lem12  9665  fpwwe2lem13  9666  fpwwe2  9667  canth4  9671  canthwelem  9674  pwfseqlem4  9686  recmulnq  9988  dmrecnq  9992  ltweuz  12968  isercolllem2  14604  isercolllem3  14605  fsumss  14664  ackbijnn  14767  fprodss  14885  1arith  15838  vdwlem1  15892  vdwlem5  15896  vdwlem6  15897  vdwlem8  15899  vdwlem11  15902  ghmpreima  17890  gicer  17926  torsubg  18464  gsumzmhm  18544  gsumzoppg  18551  lmhmpreima  19261  mplcoe5  19683  psr1baslem  19770  evpmss  20147  ofco2  20475  cnpnei  21289  cnclima  21293  iscncl  21294  cnntri  21296  cnclsi  21297  cncls2  21298  cncls  21299  cnntr  21300  cncnp  21305  cnrest2  21311  cndis  21316  2ndcomap  21482  kgencn  21580  kgencn3  21582  ptbasfi  21605  txcnmpt  21648  txdis1cn  21659  qtopval2  21720  basqtop  21735  qtopcld  21737  qtopcn  21738  qtopeu  21740  qtoprest  21741  hmeoimaf1o  21794  hmphtop  21802  hmpher  21808  ordthmeolem  21825  elfm3  21974  rnelfmlem  21976  rnelfm  21977  fmfnfmlem2  21979  fmfnfmlem4  21981  clssubg  22132  tgphaus  22140  qustgplem  22144  ucnprima  22306  ucncn  22309  xmeter  22458  imasf1oxms  22514  metustss  22576  metustexhalf  22581  metustfbas  22582  cfilucfil  22584  metuel2  22590  restmetu  22595  mbfconstlem  23615  i1fima  23665  i1fima2  23666  i1fd  23668  itg1addlem5  23687  plyeq0lem  24186  dgrcl  24209  dgrub  24210  dgrlb  24212  vieta1lem1  24285  vieta1lem2  24286  pserulm  24396  psercn2  24397  psercnlem2  24398  psercnlem1  24399  psercn  24400  pserdvlem1  24401  pserdvlem2  24402  pserdv  24403  pserdv2  24404  abelth  24415  eff1olem  24515  dvlog  24618  logtayl  24627  cxpcn3lem  24709  cxpcn3  24710  resqrtcn  24711  basellem5  25032  elnlfn  29127  nlelshi  29259  xppreima  29789  ofpreima  29805  ofpreima2  29806  ffsrn  29844  locfinreflem  30247  indpreima  30427  indf1ofs  30428  carsggect  30720  sibfof  30742  sitgclg  30744  eulerpartlemsv2  30760  eulerpartlemsf  30761  eulerpartlemv  30766  eulerpartlemb  30770  eulerpartlemt  30773  eulerpartlemr  30776  eulerpartlemgu  30779  eulerpartlemgs2  30782  eulerpartlemn  30783  cvmliftmolem1  31601  cvmlift2lem9  31631  cvmlift3lem6  31644  cvmlift3lem7  31645  mthmsta  31813  dvtan  33792  itg2addnclem  33793  ftc1anclem6  33822  sstotbnd2  33905  keridl  34163  diaintclN  36868  dibintclN  36977  dihintcl  37154  pw2f1ocnv  38130  dnnumch3lem  38142  dnnumch3  38143  pwfi2f1o  38192  binomcxplemdvbinom  39078  binomcxplemdvsum  39080  binomcxplemnotnn0  39081  wessf1ornlem  39891  sge0f1o  41116  mbfresmf  41468  smfco  41529  smfsuplem1  41537