Theorem cnvimass 5404

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

Syntax hints:   ⊆ wss 3540  ^◡ccnv 5037  dom cdm 5038  ran crn 5039   “ cima 5041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-cnv 5046  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051

This theorem is referenced by:  fvimacnvi  6239  elpreima  6245  iinpreima  6253  fconst4  6383  frnsuppeq  7194  pw2f1olem  7949  cnvimamptfin  8150  fisuppfi  8166  infxpenlem  8719  enfin2i  9026  fin1a2lem7  9111  smobeth  9287  fpwwe2lem3  9334  fpwwe2lem12  9342  fpwwe2lem13  9343  fpwwe2  9344  canth4  9348  canthwelem  9351  pwfseqlem4  9363  recmulnq  9665  dmrecnq  9669  ltweuz  12622  isercolllem2  14244  isercolllem3  14245  fsumss  14303  ackbijnn  14399  fprodss  14517  1arith  15469  vdwlem1  15523  vdwlem5  15527  vdwlem6  15528  vdwlem8  15530  vdwlem11  15533  ghmpreima  17505  gicer  17541  gicerOLD  17542  torsubg  18080  gsumzmhm  18160  gsumzoppg  18167  lmhmpreima  18869  mplcoe5  19289  psr1baslem  19376  evpmss  19751  ofco2  20076  cnpnei  20878  cnclima  20882  iscncl  20883  cnntri  20885  cnclsi  20886  cncls2  20887  cncls  20888  cnntr  20889  cncnp  20894  cnrest2  20900  cndis  20905  2ndcomap  21071  kgencn  21169  kgencn3  21171  ptbasfi  21194  txcnmpt  21237  txdis1cn  21248  qtopval2  21309  basqtop  21324  qtopcld  21326  qtopcn  21327  qtopeu  21329  qtoprest  21330  hmeoimaf1o  21383  hmphtop  21391  hmpher  21397  ordthmeolem  21414  elfm3  21564  rnelfmlem  21566  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  clssubg  21722  tgphaus  21730  qustgplem  21734  ucnprima  21896  ucncn  21899  xmeter  22048  imasf1oxms  22104  metustss  22166  metustexhalf  22171  metustfbas  22172  cfilucfil  22174  metuel2  22180  restmetu  22185  mbfconstlem  23202  i1fima  23251  i1fima2  23252  i1fd  23254  itg1addlem5  23273  plyeq0lem  23770  dgrcl  23793  dgrub  23794  dgrlb  23796  vieta1lem1  23869  vieta1lem2  23870  pserulm  23980  psercn2  23981  psercnlem2  23982  psercnlem1  23983  psercn  23984  pserdvlem1  23985  pserdvlem2  23986  pserdv  23987  pserdv2  23988  abelth  23999  eff1olem  24098  dvlog  24197  logtayl  24206  cxpcn3lem  24288  cxpcn3  24289  resqrtcn  24290  basellem5  24611  elnlfn  28171  nlelshi  28303  xppreima  28829  ofpreima  28848  ofpreima2  28849  ffsrn  28892  locfinreflem  29235  indpreima  29414  indf1ofs  29415  carsggect  29707  sibfof  29729  sitgclg  29731  eulerpartlemsv2  29747  eulerpartlemsf  29748  eulerpartlemv  29753  eulerpartlemb  29757  eulerpartlemt  29760  eulerpartlemr  29763  eulerpartlemgu  29766  eulerpartlemgs2  29769  eulerpartlemn  29770  cvmliftmolem1  30517  cvmlift2lem9  30547  cvmlift3lem6  30560  cvmlift3lem7  30561  mthmsta  30729  dvtan  32630  itg2addnclem  32631  ftc1anclem6  32660  sstotbnd2  32743  keridl  33001  diaintclN  35365  dibintclN  35474  dihintcl  35651  pw2f1ocnv  36622  dnnumch3lem  36634  dnnumch3  36635  pwfi2f1o  36684  binomcxplemdvbinom  37574  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  wessf1ornlem  38366  sge0f1o  39275  mbfresmf  39626  smfco  39687