Theorem cnvimass 6205

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

This proof depends on syntax axioms:   ⊆ wss 3900  ^◡ccnv 5654  dom cdm 5655  ran crn 5656   “ cima 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-rel 5662  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  cnvimassrndmOLD  6206  fvimacnvi  7062  elpreima  7068  cnvimainrn  7077  iinpreima  7080  rescnvimafod  7084  fconst4  7230  fsuppeq  8206  fsuppeqg  8207  pw2f1olem  9114  cnvimamptfin  9356  fisuppfi  9377  infxpenlem  10105  enfin2i  10412  fin1a2lem7  10497  smobeth  10684  fpwwe2lem3  10731  fpwwe2lem11  10739  fpwwe2lem12  10740  fpwwe2  10741  canth4  10745  canthwelem  10748  pwfseqlem4  10760  recmulnq  11062  dmrecnq  11066  ltweuz  14117  isercolllem2  15848  isercolllem3  15849  fsumss  15906  ackbijnn  16012  fprodss  16130  1arith  17120  vdwlem1  17174  vdwlem5  17178  vdwlem6  17179  vdwlem8  17181  vdwlem11  17184  ghmpreima  19467  gicer  19506  torsubg  20083  gsumzmhm  20166  gsumzoppg  20173  ricrel  20759  lmhmpreima  21338  rhmpreimaidl  21586  evpmss  21907  mplcoe5  22364  psr1baslem  22518  ofco2  22781  cnpnei  23597  cnclima  23601  iscncl  23602  cnntri  23604  cnclsi  23605  cncls2  23606  cncls  23607  cnntr  23608  cncnp  23613  cnrest2  23619  cndis  23624  2ndcomap  23792  kgencn  23890  kgencn3  23892  ptbasfi  23915  txcnmpt  23958  txdis1cn  23969  qtopval2  24030  basqtop  24045  qtopcld  24047  qtopcn  24048  qtopeu  24050  qtoprest  24051  hmeoimaf1o  24104  hmphtop  24112  hmpher  24118  ordthmeolem  24135  elfm3  24284  rnelfmlem  24286  rnelfm  24287  fmfnfmlem2  24289  fmfnfmlem4  24291  clssubg  24443  tgphaus  24451  qustgplem  24455  ucnprima  24615  ucncn  24618  xmeter  24767  imasf1oxms  24823  metustss  24885  metustexhalf  24890  metustfbas  24891  cfilucfil  24893  metuel2  24899  restmetu  24904  mbfconstlem  25963  i1fima  26014  i1fima2  26015  i1fd  26017  itg1addlem5  26036  plyeq0lem  26544  dgrcl  26567  dgrub  26568  dgrlb  26570  vieta1lem1  26648  vieta1lem2  26649  pserulm  26764  psercn2  26765  psercnlem2  26766  psercnlem1  26767  psercn  26768  pserdvlem1  26769  pserdvlem2  26770  pserdv  26771  pserdv2  26772  abelth  26783  eff1olem  26891  dvlog  26994  logtayl  27003  cxpcn3lem  27090  cxpcn3  27091  resqrtcn  27092  basellem5  27427  elnlfn  32545  nlelshi  32677  xppreima  33296  ofpreima  33316  ofpreima2  33317  fnpreimac  33321  ffsrn  33376  indpreima  33488  indf1ofs  33489  pwrssmgc  33617  elrgspnsubrunlem2  33865  elrspunidl  34034  ply1degltel  34182  ply1degleel  34183  ply1degltlss  34184  esplysply  34259  dimkerim  34315  lvecendof1f1o  34321  locfinreflem  34528  zarcmplem  34569  carsggect  35006  sibfof  35028  sitgclg  35030  eulerpartlemsv2  35046  eulerpartlemsf  35047  eulerpartlemv  35052  eulerpartlemb  35056  eulerpartlemt  35059  eulerpartlemr  35062  eulerpartlemgu  35065  eulerpartlemgs2  35068  eulerpartlemn  35069  onvfowev  36007  cvmliftmolem1  36170  cvmlift2lem9  36200  cvmlift3lem6  36213  cvmlift3lem7  36214  mthmsta  36467  dvtan  38734  itg2addnclem  38735  ftc1anclem6  38762  sstotbnd2  38854  keridl  39112  diaintclN  42261  dibintclN  42370  dihintcl  42547  pw2f1ocnv  44190  dnnumch3lem  44199  dnnumch3  44200  pwfi2f1o  44244  binomcxplemdvbinom  45483  binomcxplemdvsum  45485  binomcxplemnotnn0  45486  wessf1ornlem  46345  sge0f1o  47537  mbfresmf  47894  smfco  47957  smfsuplem1  47966  fcores  48282  3f1oss1  48290  uniimaprimaeqfv  48609  elsetpreimafvssdm  48613  gricrel  49162  grlicrel  49249