Theorem cnvimass 6198

Description: Any preimage by a 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 6197	. 2 ⊢ (◡𝐴 “ 𝐵) ⊆ ran ◡𝐴
2		dfdm4 5877	. 2 ⊢ dom 𝐴 = ran ◡𝐴
3	1, 2	sseqtrri 3980	1 ⊢ (◡𝐴 “ 𝐵) ⊆ dom 𝐴

This proof depends on syntax axioms:   ⊆ wss 3899  ^◡ccnv 5650  dom cdm 5651  ran crn 5652   “ cima 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-rel 5658  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is used by:  cnvimassrndmOLD  6199  fvimacnvi  7051  elpreima  7057  cnvimainrn  7066  iinpreima  7069  rescnvimafod  7073  fconst4  7220  fsuppeq  8192  fsuppeqg  8193  pw2f1olem  9100  cnvimamptfin  9342  fisuppfi  9363  infxpenlem  10092  enfin2i  10399  fin1a2lem7  10484  smobeth  10671  fpwwe2lem3  10718  fpwwe2lem11  10726  fpwwe2lem12  10727  fpwwe2  10728  canth4  10732  canthwelem  10735  pwfseqlem4  10747  recmulnq  11049  dmrecnq  11053  ltweuz  14104  isercolllem2  15833  isercolllem3  15834  fsumss  15891  ackbijnn  15997  fprodss  16115  1arith  17105  vdwlem1  17159  vdwlem5  17163  vdwlem6  17164  vdwlem8  17166  vdwlem11  17169  ghmpreima  19452  gicer  19491  torsubg  20068  gsumzmhm  20151  gsumzoppg  20158  ricrel  20744  lmhmpreima  21323  rhmpreimaidl  21571  evpmss  21892  mplcoe5  22349  psr1baslem  22503  ofco2  22766  cnpnei  23582  cnclima  23586  iscncl  23587  cnntri  23589  cnclsi  23590  cncls2  23591  cncls  23592  cnntr  23593  cncnp  23598  cnrest2  23604  cndis  23609  2ndcomap  23777  kgencn  23875  kgencn3  23877  ptbasfi  23900  txcnmpt  23943  txdis1cn  23954  qtopval2  24015  basqtop  24030  qtopcld  24032  qtopcn  24033  qtopeu  24035  qtoprest  24036  hmeoimaf1o  24089  hmphtop  24097  hmpher  24103  ordthmeolem  24120  elfm3  24269  rnelfmlem  24271  rnelfm  24272  fmfnfmlem2  24274  fmfnfmlem4  24276  clssubg  24428  tgphaus  24436  qustgplem  24440  ucnprima  24600  ucncn  24603  xmeter  24752  imasf1oxms  24808  metustss  24870  metustexhalf  24875  metustfbas  24876  cfilucfil  24878  metuel2  24884  restmetu  24889  mbfconstlem  25948  i1fima  25999  i1fima2  26000  i1fd  26002  itg1addlem5  26021  plyeq0lem  26529  dgrcl  26552  dgrub  26553  dgrlb  26555  vieta1lem1  26633  vieta1lem2  26634  pserulm  26749  psercn2  26750  psercnlem2  26751  psercnlem1  26752  psercn  26753  pserdvlem1  26754  pserdvlem2  26755  pserdv  26756  pserdv2  26757  abelth  26768  eff1olem  26876  dvlog  26979  logtayl  26988  cxpcn3lem  27075  cxpcn3  27076  resqrtcn  27077  basellem5  27412  elnlfn  32530  nlelshi  32662  xppreima  33239  ofpreima  33259  ofpreima2  33260  fnpreimac  33264  ffsrn  33320  indpreima  33432  indf1ofs  33433  pwrssmgc  33561  elrgspnsubrunlem2  33809  elrspunidl  33978  ply1degltel  34126  ply1degleel  34127  ply1degltlss  34128  esplysply  34203  dimkerim  34259  lvecendof1f1o  34265  locfinreflem  34472  zarcmplem  34513  carsggect  34950  sibfof  34972  sitgclg  34974  eulerpartlemsv2  34990  eulerpartlemsf  34991  eulerpartlemv  34996  eulerpartlemb  35000  eulerpartlemt  35003  eulerpartlemr  35006  eulerpartlemgu  35009  eulerpartlemgs2  35012  eulerpartlemn  35013  onvfowev  35899  cvmliftmolem1  36046  cvmlift2lem9  36076  cvmlift3lem6  36089  cvmlift3lem7  36090  mthmsta  36343  dvtan  38588  itg2addnclem  38589  ftc1anclem6  38616  sstotbnd2  38708  keridl  38966  diaintclN  42115  dibintclN  42224  dihintcl  42401  pw2f1ocnv  44043  dnnumch3lem  44052  dnnumch3  44053  pwfi2f1o  44097  binomcxplemdvbinom  45336  binomcxplemdvsum  45338  binomcxplemnotnn0  45339  wessf1ornlem  46199  sge0f1o  47391  mbfresmf  47748  smfco  47811  smfsuplem1  47820  fcores  48136  3f1oss1  48144  uniimaprimaeqfv  48463  elsetpreimafvssdm  48467  gricrel  49016  grlicrel  49103