Theorem cnvimass 6033

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

Syntax hints:   ⊆ wss 3903  ^◡ccnv 5618  dom cdm 5619  ran crn 5620   “ cima 5622

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 5235  ax-nul 5245  ax-pr 5371

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5093  df-opab 5155  df-xp 5625  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632

This theorem is referenced by:  cnvimassrndm  6101  fvimacnvi  6986  elpreima  6992  cnvimainrn  7001  iinpreima  7003  rescnvimafod  7007  fconst4  7150  fsuppeq  8108  fsuppeqg  8109  pw2f1olem  8998  cnvimamptfin  9243  fisuppfi  9261  infxpenlem  9907  enfin2i  10215  fin1a2lem7  10300  smobeth  10480  fpwwe2lem3  10527  fpwwe2lem11  10535  fpwwe2lem12  10536  fpwwe2  10537  canth4  10541  canthwelem  10544  pwfseqlem4  10556  recmulnq  10858  dmrecnq  10862  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  19117  gicer  19156  torsubg  19733  gsumzmhm  19816  gsumzoppg  19823  lmhmpreima  20952  rhmpreimaidl  21184  evpmss  21493  mplcoe5  21945  psr1baslem  22067  ofco2  22336  cnpnei  23149  cnclima  23153  iscncl  23154  cnntri  23156  cnclsi  23157  cncls2  23158  cncls  23159  cnntr  23160  cncnp  23165  cnrest2  23171  cndis  23176  2ndcomap  23343  kgencn  23441  kgencn3  23443  ptbasfi  23466  txcnmpt  23509  txdis1cn  23520  qtopval2  23581  basqtop  23596  qtopcld  23598  qtopcn  23599  qtopeu  23601  qtoprest  23602  hmeoimaf1o  23655  hmphtop  23663  hmpher  23669  ordthmeolem  23686  elfm3  23835  rnelfmlem  23837  rnelfm  23838  fmfnfmlem2  23840  fmfnfmlem4  23842  clssubg  23994  tgphaus  24002  qustgplem  24006  ucnprima  24167  ucncn  24170  xmeter  24319  imasf1oxms  24375  metustss  24437  metustexhalf  24442  metustfbas  24443  cfilucfil  24445  metuel2  24451  restmetu  24456  mbfconstlem  25526  i1fima  25577  i1fima2  25578  i1fd  25580  itg1addlem5  25599  plyeq0lem  26113  dgrcl  26136  dgrub  26137  dgrlb  26139  vieta1lem1  26216  vieta1lem2  26217  pserulm  26329  psercn2  26330  psercn2OLD  26331  psercnlem2  26332  psercnlem1  26333  psercn  26334  pserdvlem1  26335  pserdvlem2  26336  pserdv  26337  pserdv2  26338  abelth  26349  eff1olem  26455  dvlog  26558  logtayl  26567  cxpcn3lem  26655  cxpcn3  26656  resqrtcn  26657  basellem5  26993  elnlfn  31872  nlelshi  32004  xppreima  32589  ofpreima  32609  ofpreima2  32610  fnpreimac  32615  ffsrn  32673  indpreima  32809  indf1ofs  32810  pwrssmgc  32943  elrgspnsubrunlem2  33189  elrspunidl  33366  ply1degltel  33528  ply1degleel  33529  ply1degltlss  33530  dimkerim  33600  lvecendof1f1o  33606  locfinreflem  33813  zarcmplem  33854  carsggect  34292  sibfof  34314  sitgclg  34316  eulerpartlemsv2  34332  eulerpartlemsf  34333  eulerpartlemv  34338  eulerpartlemb  34342  eulerpartlemt  34345  eulerpartlemr  34348  eulerpartlemgu  34351  eulerpartlemgs2  34354  eulerpartlemn  34355  cvmliftmolem1  35264  cvmlift2lem9  35294  cvmlift3lem6  35307  cvmlift3lem7  35308  mthmsta  35561  dvtan  37660  itg2addnclem  37661  ftc1anclem6  37688  sstotbnd2  37764  keridl  38022  diaintclN  41047  dibintclN  41156  dihintcl  41333  pw2f1ocnv  43020  dnnumch3lem  43029  dnnumch3  43030  pwfi2f1o  43079  binomcxplemdvbinom  44336  binomcxplemdvsum  44338  binomcxplemnotnn0  44339  wessf1ornlem  45173  sge0f1o  46373  mbfresmf  46730  smfco  46793  smfsuplem1  46802  fcores  47061  3f1oss1  47069  uniimaprimaeqfv  47376  elsetpreimafvssdm  47380  gricrel  47913  grlicrel  48000