Theorem cnvimass 5934

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

Syntax hints:   ⊆ wss 3853  ^◡ccnv 5535  dom cdm 5536  ran crn 5537   “ cima 5539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040  df-opab 5102  df-xp 5542  df-cnv 5544  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549

This theorem is referenced by:  cnvimassrndm  5995  fvimacnvi  6850  elpreima  6856  cnvimainrn  6865  iinpreima  6867  rescnvimafod  6872  fconst4  7008  frnsuppeq  7895  frnsuppeqg  7896  pw2f1olem  8727  cnvimamptfin  8955  fisuppfi  8971  infxpenlem  9592  enfin2i  9900  fin1a2lem7  9985  smobeth  10165  fpwwe2lem3  10212  fpwwe2lem11  10220  fpwwe2lem12  10221  fpwwe2  10222  canth4  10226  canthwelem  10229  pwfseqlem4  10241  recmulnq  10543  dmrecnq  10547  ltweuz  13499  isercolllem2  15194  isercolllem3  15195  fsumss  15254  ackbijnn  15355  fprodss  15473  1arith  16443  vdwlem1  16497  vdwlem5  16501  vdwlem6  16502  vdwlem8  16504  vdwlem11  16507  ghmpreima  18598  gicer  18634  torsubg  19193  gsumzmhm  19276  gsumzoppg  19283  lmhmpreima  20039  evpmss  20502  mplcoe5  20951  psr1baslem  21060  ofco2  21302  cnpnei  22115  cnclima  22119  iscncl  22120  cnntri  22122  cnclsi  22123  cncls2  22124  cncls  22125  cnntr  22126  cncnp  22131  cnrest2  22137  cndis  22142  2ndcomap  22309  kgencn  22407  kgencn3  22409  ptbasfi  22432  txcnmpt  22475  txdis1cn  22486  qtopval2  22547  basqtop  22562  qtopcld  22564  qtopcn  22565  qtopeu  22567  qtoprest  22568  hmeoimaf1o  22621  hmphtop  22629  hmpher  22635  ordthmeolem  22652  elfm3  22801  rnelfmlem  22803  rnelfm  22804  fmfnfmlem2  22806  fmfnfmlem4  22808  clssubg  22960  tgphaus  22968  qustgplem  22972  ucnprima  23133  ucncn  23136  xmeter  23285  imasf1oxms  23341  metustss  23403  metustexhalf  23408  metustfbas  23409  cfilucfil  23411  metuel2  23417  restmetu  23422  mbfconstlem  24478  i1fima  24529  i1fima2  24530  i1fd  24532  itg1addlem5  24552  plyeq0lem  25058  dgrcl  25081  dgrub  25082  dgrlb  25084  vieta1lem1  25157  vieta1lem2  25158  pserulm  25268  psercn2  25269  psercnlem2  25270  psercnlem1  25271  psercn  25272  pserdvlem1  25273  pserdvlem2  25274  pserdv  25275  pserdv2  25276  abelth  25287  eff1olem  25391  dvlog  25493  logtayl  25502  cxpcn3lem  25587  cxpcn3  25588  resqrtcn  25589  basellem5  25921  elnlfn  29963  nlelshi  30095  xppreima  30656  ofpreima  30676  ofpreima2  30677  fnpreimac  30682  ffsrn  30738  pwrssmgc  30951  rhmpreimaidl  31271  elrspunidl  31274  dimkerim  31376  locfinreflem  31458  zarcmplem  31499  indpreima  31659  indf1ofs  31660  carsggect  31951  sibfof  31973  sitgclg  31975  eulerpartlemsv2  31991  eulerpartlemsf  31992  eulerpartlemv  31997  eulerpartlemb  32001  eulerpartlemt  32004  eulerpartlemr  32007  eulerpartlemgu  32010  eulerpartlemgs2  32013  eulerpartlemn  32014  cvmliftmolem1  32910  cvmlift2lem9  32940  cvmlift3lem6  32953  cvmlift3lem7  32954  mthmsta  33207  dvtan  35513  itg2addnclem  35514  ftc1anclem6  35541  sstotbnd2  35618  keridl  35876  diaintclN  38758  dibintclN  38867  dihintcl  39044  pw2f1ocnv  40503  dnnumch3lem  40515  dnnumch3  40516  pwfi2f1o  40565  binomcxplemdvbinom  41585  binomcxplemdvsum  41587  binomcxplemnotnn0  41588  wessf1ornlem  42336  sge0f1o  43538  mbfresmf  43890  smfco  43951  smfsuplem1  43959  fcores  44176  uniimaprimaeqfv  44450  elsetpreimafvssdm  44454