Theorem cnvimass 6042

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

Syntax hints:   ⊆ wss 3911  ^◡ccnv 5630  dom cdm 5631  ran crn 5632   “ cima 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  cnvimassrndm  6113  fvimacnvi  7006  elpreima  7012  cnvimainrn  7021  iinpreima  7023  rescnvimafod  7027  fconst4  7170  fsuppeq  8131  fsuppeqg  8132  pw2f1olem  9022  cnvimamptfin  9280  fisuppfi  9298  infxpenlem  9942  enfin2i  10250  fin1a2lem7  10335  smobeth  10515  fpwwe2lem3  10562  fpwwe2lem11  10570  fpwwe2lem12  10571  fpwwe2  10572  canth4  10576  canthwelem  10579  pwfseqlem4  10591  recmulnq  10893  dmrecnq  10897  ltweuz  13902  isercolllem2  15608  isercolllem3  15609  fsumss  15667  ackbijnn  15770  fprodss  15890  1arith  16874  vdwlem1  16928  vdwlem5  16932  vdwlem6  16933  vdwlem8  16935  vdwlem11  16938  ghmpreima  19152  gicer  19191  torsubg  19768  gsumzmhm  19851  gsumzoppg  19858  lmhmpreima  20987  rhmpreimaidl  21219  evpmss  21528  mplcoe5  21980  psr1baslem  22102  ofco2  22371  cnpnei  23184  cnclima  23188  iscncl  23189  cnntri  23191  cnclsi  23192  cncls2  23193  cncls  23194  cnntr  23195  cncnp  23200  cnrest2  23206  cndis  23211  2ndcomap  23378  kgencn  23476  kgencn3  23478  ptbasfi  23501  txcnmpt  23544  txdis1cn  23555  qtopval2  23616  basqtop  23631  qtopcld  23633  qtopcn  23634  qtopeu  23636  qtoprest  23637  hmeoimaf1o  23690  hmphtop  23698  hmpher  23704  ordthmeolem  23721  elfm3  23870  rnelfmlem  23872  rnelfm  23873  fmfnfmlem2  23875  fmfnfmlem4  23877  clssubg  24029  tgphaus  24037  qustgplem  24041  ucnprima  24202  ucncn  24205  xmeter  24354  imasf1oxms  24410  metustss  24472  metustexhalf  24477  metustfbas  24478  cfilucfil  24480  metuel2  24486  restmetu  24491  mbfconstlem  25561  i1fima  25612  i1fima2  25613  i1fd  25615  itg1addlem5  25634  plyeq0lem  26148  dgrcl  26171  dgrub  26172  dgrlb  26174  vieta1lem1  26251  vieta1lem2  26252  pserulm  26364  psercn2  26365  psercn2OLD  26366  psercnlem2  26367  psercnlem1  26368  psercn  26369  pserdvlem1  26370  pserdvlem2  26371  pserdv  26372  pserdv2  26373  abelth  26384  eff1olem  26490  dvlog  26593  logtayl  26602  cxpcn3lem  26690  cxpcn3  26691  resqrtcn  26692  basellem5  27028  elnlfn  31907  nlelshi  32039  xppreima  32619  ofpreima  32639  ofpreima2  32640  fnpreimac  32645  ffsrn  32702  indpreima  32838  indf1ofs  32839  pwrssmgc  32972  elrgspnsubrunlem2  33215  elrspunidl  33392  ply1degltel  33553  ply1degleel  33554  ply1degltlss  33555  dimkerim  33616  lvecendof1f1o  33622  locfinreflem  33823  zarcmplem  33864  carsggect  34302  sibfof  34324  sitgclg  34326  eulerpartlemsv2  34342  eulerpartlemsf  34343  eulerpartlemv  34348  eulerpartlemb  34352  eulerpartlemt  34355  eulerpartlemr  34358  eulerpartlemgu  34361  eulerpartlemgs2  34364  eulerpartlemn  34365  cvmliftmolem1  35261  cvmlift2lem9  35291  cvmlift3lem6  35304  cvmlift3lem7  35305  mthmsta  35558  dvtan  37657  itg2addnclem  37658  ftc1anclem6  37685  sstotbnd2  37761  keridl  38019  diaintclN  41045  dibintclN  41154  dihintcl  41331  pw2f1ocnv  43019  dnnumch3lem  43028  dnnumch3  43029  pwfi2f1o  43078  binomcxplemdvbinom  44335  binomcxplemdvsum  44337  binomcxplemnotnn0  44338  wessf1ornlem  45172  sge0f1o  46373  mbfresmf  46730  smfco  46793  smfsuplem1  46802  fcores  47061  3f1oss1  47069  uniimaprimaeqfv  47376  elsetpreimafvssdm  47380  gricrel  47912  grlicrel  47991