Theorem cnvimass 5943

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

Syntax hints:   ⊆ wss 3935  ^◡ccnv 5548  dom cdm 5549  ran crn 5550   “ cima 5552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-br 5059  df-opab 5121  df-xp 5555  df-cnv 5557  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562

This theorem is referenced by:  fvimacnvi  6816  elpreima  6822  iinpreima  6831  fconst4  6971  frnsuppeq  7836  pw2f1olem  8615  cnvimamptfin  8819  fisuppfi  8835  infxpenlem  9433  enfin2i  9737  fin1a2lem7  9822  smobeth  10002  fpwwe2lem3  10049  fpwwe2lem12  10057  fpwwe2lem13  10058  fpwwe2  10059  canth4  10063  canthwelem  10066  pwfseqlem4  10078  recmulnq  10380  dmrecnq  10384  ltweuz  13323  isercolllem2  15016  isercolllem3  15017  fsumss  15076  ackbijnn  15177  fprodss  15296  1arith  16257  vdwlem1  16311  vdwlem5  16315  vdwlem6  16316  vdwlem8  16318  vdwlem11  16321  ghmpreima  18374  gicer  18410  torsubg  18968  gsumzmhm  19051  gsumzoppg  19058  lmhmpreima  19814  mplcoe5  20243  psr1baslem  20347  evpmss  20724  ofco2  21054  cnpnei  21866  cnclima  21870  iscncl  21871  cnntri  21873  cnclsi  21874  cncls2  21875  cncls  21876  cnntr  21877  cncnp  21882  cnrest2  21888  cndis  21893  2ndcomap  22060  kgencn  22158  kgencn3  22160  ptbasfi  22183  txcnmpt  22226  txdis1cn  22237  qtopval2  22298  basqtop  22313  qtopcld  22315  qtopcn  22316  qtopeu  22318  qtoprest  22319  hmeoimaf1o  22372  hmphtop  22380  hmpher  22386  ordthmeolem  22403  elfm3  22552  rnelfmlem  22554  rnelfm  22555  fmfnfmlem2  22557  fmfnfmlem4  22559  clssubg  22711  tgphaus  22719  qustgplem  22723  ucnprima  22885  ucncn  22888  xmeter  23037  imasf1oxms  23093  metustss  23155  metustexhalf  23160  metustfbas  23161  cfilucfil  23163  metuel2  23169  restmetu  23174  mbfconstlem  24222  i1fima  24273  i1fima2  24274  i1fd  24276  itg1addlem5  24295  plyeq0lem  24794  dgrcl  24817  dgrub  24818  dgrlb  24820  vieta1lem1  24893  vieta1lem2  24894  pserulm  25004  psercn2  25005  psercnlem2  25006  psercnlem1  25007  psercn  25008  pserdvlem1  25009  pserdvlem2  25010  pserdv  25011  pserdv2  25012  abelth  25023  eff1olem  25126  dvlog  25228  logtayl  25237  cxpcn3lem  25322  cxpcn3  25323  resqrtcn  25324  basellem5  25656  elnlfn  29699  nlelshi  29831  xppreima  30388  ofpreima  30404  ofpreima2  30405  fnpreimac  30410  ffsrn  30459  dimkerim  31018  locfinreflem  31099  indpreima  31279  indf1ofs  31280  carsggect  31571  sibfof  31593  sitgclg  31595  eulerpartlemsv2  31611  eulerpartlemsf  31612  eulerpartlemv  31617  eulerpartlemb  31621  eulerpartlemt  31624  eulerpartlemr  31627  eulerpartlemgu  31630  eulerpartlemgs2  31633  eulerpartlemn  31634  cvmliftmolem1  32523  cvmlift2lem9  32553  cvmlift3lem6  32566  cvmlift3lem7  32567  mthmsta  32820  dvtan  34936  itg2addnclem  34937  ftc1anclem6  34966  sstotbnd2  35046  keridl  35304  diaintclN  38188  dibintclN  38297  dihintcl  38474  pw2f1ocnv  39627  dnnumch3lem  39639  dnnumch3  39640  pwfi2f1o  39689  binomcxplemdvbinom  40678  binomcxplemdvsum  40680  binomcxplemnotnn0  40681  wessf1ornlem  41438  sge0f1o  42658  mbfresmf  43010  smfco  43071  smfsuplem1  43079  uniimaprimaeqfv  43536  elsetpreimafvssdm  43540