Theorem cnvimass 5789

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

Syntax hints:   ⊆ wss 3829  ^◡ccnv 5406  dom cdm 5407  ran crn 5408   “ cima 5410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pr 5186

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-br 4930  df-opab 4992  df-xp 5413  df-cnv 5415  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420

This theorem is referenced by:  fvimacnvi  6647  elpreima  6653  iinpreima  6662  fconst4  6803  frnsuppeq  7645  pw2f1olem  8417  cnvimamptfin  8620  fisuppfi  8636  infxpenlem  9233  enfin2i  9541  fin1a2lem7  9626  smobeth  9806  fpwwe2lem3  9853  fpwwe2lem12  9861  fpwwe2lem13  9862  fpwwe2  9863  canth4  9867  canthwelem  9870  pwfseqlem4  9882  recmulnq  10184  dmrecnq  10188  ltweuz  13144  isercolllem2  14883  isercolllem3  14884  fsumss  14942  ackbijnn  15043  fprodss  15162  1arith  16119  vdwlem1  16173  vdwlem5  16177  vdwlem6  16178  vdwlem8  16180  vdwlem11  16183  ghmpreima  18151  gicer  18187  torsubg  18730  gsumzmhm  18810  gsumzoppg  18817  lmhmpreima  19542  mplcoe5  19962  psr1baslem  20056  evpmss  20432  ofco2  20764  cnpnei  21576  cnclima  21580  iscncl  21581  cnntri  21583  cnclsi  21584  cncls2  21585  cncls  21586  cnntr  21587  cncnp  21592  cnrest2  21598  cndis  21603  2ndcomap  21770  kgencn  21868  kgencn3  21870  ptbasfi  21893  txcnmpt  21936  txdis1cn  21947  qtopval2  22008  basqtop  22023  qtopcld  22025  qtopcn  22026  qtopeu  22028  qtoprest  22029  hmeoimaf1o  22082  hmphtop  22090  hmpher  22096  ordthmeolem  22113  elfm3  22262  rnelfmlem  22264  rnelfm  22265  fmfnfmlem2  22267  fmfnfmlem4  22269  clssubg  22420  tgphaus  22428  qustgplem  22432  ucnprima  22594  ucncn  22597  xmeter  22746  imasf1oxms  22802  metustss  22864  metustexhalf  22869  metustfbas  22870  cfilucfil  22872  metuel2  22878  restmetu  22883  mbfconstlem  23931  i1fima  23982  i1fima2  23983  i1fd  23985  itg1addlem5  24004  plyeq0lem  24503  dgrcl  24526  dgrub  24527  dgrlb  24529  vieta1lem1  24602  vieta1lem2  24603  pserulm  24713  psercn2  24714  psercnlem2  24715  psercnlem1  24716  psercn  24717  pserdvlem1  24718  pserdvlem2  24719  pserdv  24720  pserdv2  24721  abelth  24732  eff1olem  24833  dvlog  24935  logtayl  24944  cxpcn3lem  25029  cxpcn3  25030  resqrtcn  25031  basellem5  25364  elnlfn  29486  nlelshi  29618  xppreima  30156  ofpreima  30172  ofpreima2  30173  fnpreimac  30178  ffsrn  30224  dimkerim  30658  locfinreflem  30754  indpreima  30934  indf1ofs  30935  carsggect  31227  sibfof  31249  sitgclg  31251  eulerpartlemsv2  31267  eulerpartlemsf  31268  eulerpartlemv  31273  eulerpartlemb  31277  eulerpartlemt  31280  eulerpartlemr  31283  eulerpartlemgu  31286  eulerpartlemgs2  31289  eulerpartlemn  31290  cvmliftmolem1  32119  cvmlift2lem9  32149  cvmlift3lem6  32162  cvmlift3lem7  32163  mthmsta  32351  dvtan  34389  itg2addnclem  34390  ftc1anclem6  34419  sstotbnd2  34500  keridl  34758  diaintclN  37645  dibintclN  37754  dihintcl  37931  pw2f1ocnv  39036  dnnumch3lem  39048  dnnumch3  39049  pwfi2f1o  39098  binomcxplemdvbinom  40107  binomcxplemdvsum  40109  binomcxplemnotnn0  40110  wessf1ornlem  40875  sge0f1o  42101  mbfresmf  42453  smfco  42514  smfsuplem1  42522