Theorem cnvimass 6086

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

This proof depends on syntax axioms:   ⊆ wss 3906  ^◡ccnv 5662  dom cdm 5663  ran crn 5664   “ cima 5666

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is used by:  cnvimassrndm  6151  fvimacnvi  7052  elpreima  7058  cnvimainrn  7067  iinpreima  7069  rescnvimafod  7073  fconst4  7220  fsuppeq  8178  fsuppeqg  8179  pw2f1olem  9077  cnvimamptfin  9318  fisuppfi  9339  infxpenlem  10014  enfin2i  10321  fin1a2lem7  10406  smobeth  10591  fpwwe2lem3  10638  fpwwe2lem11  10646  fpwwe2lem12  10647  fpwwe2  10648  canth4  10652  canthwelem  10655  pwfseqlem4  10667  recmulnq  10969  dmrecnq  10973  ltweuz  14020  isercolllem2  15746  isercolllem3  15747  fsumss  15804  ackbijnn  15910  fprodss  16030  1arith  17014  vdwlem1  17068  vdwlem5  17072  vdwlem6  17073  vdwlem8  17075  vdwlem11  17078  ghmpreima  19357  gicer  19396  torsubg  19973  gsumzmhm  20056  gsumzoppg  20063  ricrel  20647  lmhmpreima  21224  rhmpreimaidl  21471  evpmss  21791  mplcoe5  22246  psr1baslem  22400  ofco2  22663  cnpnei  23476  cnclima  23480  iscncl  23481  cnntri  23483  cnclsi  23484  cncls2  23485  cncls  23486  cnntr  23487  cncnp  23492  cnrest2  23498  cndis  23503  2ndcomap  23671  kgencn  23769  kgencn3  23771  ptbasfi  23794  txcnmpt  23837  txdis1cn  23848  qtopval2  23909  basqtop  23924  qtopcld  23926  qtopcn  23927  qtopeu  23929  qtoprest  23930  hmeoimaf1o  23983  hmphtop  23991  hmpher  23997  ordthmeolem  24014  elfm3  24163  rnelfmlem  24165  rnelfm  24166  fmfnfmlem2  24168  fmfnfmlem4  24170  clssubg  24322  tgphaus  24330  qustgplem  24334  ucnprima  24494  ucncn  24497  xmeter  24646  imasf1oxms  24702  metustss  24764  metustexhalf  24769  metustfbas  24770  cfilucfil  24772  metuel2  24778  restmetu  24783  mbfconstlem  25842  i1fima  25893  i1fima2  25894  i1fd  25896  itg1addlem5  25915  plyeq0lem  26423  dgrcl  26446  dgrub  26447  dgrlb  26449  vieta1lem1  26527  vieta1lem2  26528  pserulm  26641  psercn2  26642  psercnlem2  26643  psercnlem1  26644  psercn  26645  pserdvlem1  26646  pserdvlem2  26647  pserdv  26648  pserdv2  26649  abelth  26660  eff1olem  26769  dvlog  26872  logtayl  26881  cxpcn3lem  26968  cxpcn3  26969  resqrtcn  26970  basellem5  27305  elnlfn  32356  nlelshi  32488  xppreima  33066  ofpreima  33086  ofpreima2  33087  fnpreimac  33091  ffsrn  33148  indpreima  33260  indf1ofs  33261  pwrssmgc  33389  elrgspnsubrunlem2  33637  elrspunidl  33805  ply1degltel  33953  ply1degleel  33954  ply1degltlss  33955  esplysply  34030  dimkerim  34086  lvecendof1f1o  34092  locfinreflem  34299  zarcmplem  34340  carsggect  34778  sibfof  34800  sitgclg  34802  eulerpartlemsv2  34818  eulerpartlemsf  34819  eulerpartlemv  34824  eulerpartlemb  34828  eulerpartlemt  34831  eulerpartlemr  34834  eulerpartlemgu  34837  eulerpartlemgs2  34840  eulerpartlemn  34841  onvfowev  35662  cvmliftmolem1  35815  cvmlift2lem9  35845  cvmlift3lem6  35858  cvmlift3lem7  35859  mthmsta  36112  dvtan  38383  itg2addnclem  38384  ftc1anclem6  38411  sstotbnd2  38488  keridl  38746  diaintclN  41895  dibintclN  42004  dihintcl  42181  pw2f1ocnv  43842  dnnumch3lem  43851  dnnumch3  43852  pwfi2f1o  43901  binomcxplemdvbinom  45141  binomcxplemdvsum  45143  binomcxplemnotnn0  45144  wessf1ornlem  45981  sge0f1o  47174  mbfresmf  47531  smfco  47594  smfsuplem1  47603  fcores  47882  3f1oss1  47890  uniimaprimaeqfv  48209  elsetpreimafvssdm  48213  gricrel  48762  grlicrel  48849