Theorem cnvimass 6086

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

Syntax hints:   ⊆ wss 3944  ^◡ccnv 5677  dom cdm 5678  ran crn 5679   “ cima 5681

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-xp 5684  df-cnv 5686  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691

This theorem is referenced by:  cnvimassrndm  6158  fvimacnvi  7060  elpreima  7066  cnvimainrn  7075  iinpreima  7077  rescnvimafod  7082  fconst4  7226  fsuppeq  8180  fsuppeqg  8181  pw2f1olem  9101  cnvimamptfin  9379  fisuppfi  9397  infxpenlem  10038  enfin2i  10346  fin1a2lem7  10431  smobeth  10611  fpwwe2lem3  10658  fpwwe2lem11  10666  fpwwe2lem12  10667  fpwwe2  10668  canth4  10672  canthwelem  10675  pwfseqlem4  10687  recmulnq  10989  dmrecnq  10993  ltweuz  13962  isercolllem2  15648  isercolllem3  15649  fsumss  15707  ackbijnn  15810  fprodss  15928  1arith  16899  vdwlem1  16953  vdwlem5  16957  vdwlem6  16958  vdwlem8  16960  vdwlem11  16963  ghmpreima  19201  gicer  19240  torsubg  19821  gsumzmhm  19904  gsumzoppg  19911  lmhmpreima  20945  rhmpreimaidl  21184  evpmss  21535  mplcoe5  22000  psr1baslem  22127  ofco2  22397  cnpnei  23212  cnclima  23216  iscncl  23217  cnntri  23219  cnclsi  23220  cncls2  23221  cncls  23222  cnntr  23223  cncnp  23228  cnrest2  23234  cndis  23239  2ndcomap  23406  kgencn  23504  kgencn3  23506  ptbasfi  23529  txcnmpt  23572  txdis1cn  23583  qtopval2  23644  basqtop  23659  qtopcld  23661  qtopcn  23662  qtopeu  23664  qtoprest  23665  hmeoimaf1o  23718  hmphtop  23726  hmpher  23732  ordthmeolem  23749  elfm3  23898  rnelfmlem  23900  rnelfm  23901  fmfnfmlem2  23903  fmfnfmlem4  23905  clssubg  24057  tgphaus  24065  qustgplem  24069  ucnprima  24231  ucncn  24234  xmeter  24383  imasf1oxms  24442  metustss  24504  metustexhalf  24509  metustfbas  24510  cfilucfil  24512  metuel2  24518  restmetu  24523  mbfconstlem  25600  i1fima  25651  i1fima2  25652  i1fd  25654  itg1addlem5  25674  plyeq0lem  26189  dgrcl  26212  dgrub  26213  dgrlb  26215  vieta1lem1  26290  vieta1lem2  26291  pserulm  26403  psercn2  26404  psercn2OLD  26405  psercnlem2  26406  psercnlem1  26407  psercn  26408  pserdvlem1  26409  pserdvlem2  26410  pserdv  26411  pserdv2  26412  abelth  26423  eff1olem  26527  dvlog  26630  logtayl  26639  cxpcn3lem  26727  cxpcn3  26728  resqrtcn  26729  basellem5  27062  elnlfn  31810  nlelshi  31942  xppreima  32513  ofpreima  32532  ofpreima2  32533  fnpreimac  32538  ffsrn  32593  pwrssmgc  32816  elrspunidl  33240  ply1degltel  33396  ply1degleel  33397  ply1degltlss  33398  dimkerim  33456  locfinreflem  33572  zarcmplem  33613  indpreima  33775  indf1ofs  33776  carsggect  34069  sibfof  34091  sitgclg  34093  eulerpartlemsv2  34109  eulerpartlemsf  34110  eulerpartlemv  34115  eulerpartlemb  34119  eulerpartlemt  34122  eulerpartlemr  34125  eulerpartlemgu  34128  eulerpartlemgs2  34131  eulerpartlemn  34132  cvmliftmolem1  35022  cvmlift2lem9  35052  cvmlift3lem6  35065  cvmlift3lem7  35066  mthmsta  35319  dvtan  37274  itg2addnclem  37275  ftc1anclem6  37302  sstotbnd2  37378  keridl  37636  diaintclN  40661  dibintclN  40770  dihintcl  40947  pw2f1ocnv  42600  dnnumch3lem  42612  dnnumch3  42613  pwfi2f1o  42662  binomcxplemdvbinom  43932  binomcxplemdvsum  43934  binomcxplemnotnn0  43935  wessf1ornlem  44697  sge0f1o  45908  mbfresmf  46265  smfco  46328  smfsuplem1  46337  fcores  46587  uniimaprimaeqfv  46859  elsetpreimafvssdm  46863  gricrel  47371