MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  reximdv Unicode version

Theorem reximdv 2667
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)
Hypothesis
Ref Expression
reximdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
reximdv  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem reximdv
StepHypRef Expression
1 reximdv.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21a1d 22 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2666 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  r19.12  2669  reusv3  4558  iunpw  4586  fvelima  5590  frxp  6241  ssfi  7099  ordtypelem2  7250  wdom2d  7310  xpwdomg  7315  cff1  7900  iunfo  8177  nqereu  8569  reclem3pr  8689  map2psrpr  8748  supsrlem  8749  1re  8853  sswrd  11439  o1lo1  12027  rlimcn1  12078  subcn2  12084  lo1add  12116  lo1mul  12117  pythagtriplem19  12902  vdwnnlem2  13059  ramub2  13077  sylow2alem2  14945  lsmless2x  14972  efgrelexlemb  15075  tgcl  16723  neiss  16862  ssnei2  16869  tgcnp  16999  cnpco  17012  cnpresti  17032  lmcnp  17048  hausnei2  17097  1stcrest  17195  nlly2i  17218  llyss  17221  nllyss  17222  txcnpi  17318  txcmplem1  17351  tx1stc  17360  nrmr0reg  17456  fbssfi  17548  fbfinnfr  17552  fgcl  17589  ufinffr  17640  elfm2  17659  fmfnfmlem1  17665  fmco  17672  fbflim2  17688  flffbas  17706  flftg  17707  cnpflf2  17711  alexsubALT  17761  blssex  17989  mopni3  18056  neibl  18063  metss  18070  metcnp3  18102  rescncf  18417  lebnum  18478  xlebnum  18479  lebnumii  18480  lmmbr  18700  fgcfil  18713  ovolsslem  18859  ovolunlem1  18872  ovoliunnul  18882  itgcn  19213  ellimc3  19245  c1lip3  19362  itgsubstlem  19411  plyss  19597  ulmclm  19782  ulmcau  19788  ulmcn  19792  rlimcxp  20284  chtppilimlem2  20639  chtppilim  20640  isgrpo  20879  opidon  21005  rngmgmbs4  21100  tpr2rico  23311  esumpcvgval  23461  conpcon  23781  cvmliftlem15  23844  cvmlift2lem10  23858  exopcopn  25675  limptlimpr2lem1  25677  tethpnc2  26174  reftr  26392  fnessref  26396  fdc1  26559  sstotbnd3  26603  totbndss  26604  heibor1lem  26636  heibor1  26637  fiphp3d  27005  pell1qrss14  27056  infrglb  27825  stoweidlem27  27879  stoweidlem35  27887  stoweidlem48  27900  stoweidlem62  27914  afvelima  28135  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv4e  28414  lvoli2  30392  paddss2  30629  lhpexle1lem  30818  lhpexle2lem  30820  dvhdimlem  32256  dvh3dim3N  32261  mapdh9a  32602  hdmap11lem2  32657
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-ral 2561  df-rex 2562
  Copyright terms: Public domain W3C validator