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

Theorem reximdv 2625
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 24 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2624 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   E.wrex 2517
This theorem is referenced by:  r19.12  2627  reusv3  4479  iunpw  4507  fvelima  5473  frxp  6124  ssfi  7016  ordtypelem2  7167  wdom2d  7227  xpwdomg  7232  cff1  7817  iunfo  8094  nqereu  8486  reclem3pr  8606  map2psrpr  8665  supsrlem  8666  1re  8770  sswrd  11353  o1lo1  11941  rlimcn1  11992  subcn2  11998  lo1add  12030  lo1mul  12031  pythagtriplem19  12813  vdwnnlem2  12970  ramub2  12988  sylow2alem2  14856  lsmless2x  14883  efgrelexlemb  14986  tgcl  16634  neiss  16773  ssnei2  16780  tgcnp  16910  cnpco  16923  cnpresti  16943  lmcnp  16959  hausnei2  17008  1stcrest  17106  nlly2i  17129  llyss  17132  nllyss  17133  txcnpi  17229  txcmplem1  17262  tx1stc  17271  nrmr0reg  17367  fbssfi  17459  fbfinnfr  17463  fgcl  17500  ufinffr  17551  elfm2  17570  fmfnfmlem1  17576  fmco  17583  fbflim2  17599  flffbas  17617  flftg  17618  cnpflf2  17622  alexsubALT  17672  blssex  17900  mopni3  17967  neibl  17974  metss  17981  metcnp3  18013  rescncf  18328  lebnum  18389  xlebnum  18390  lebnumii  18391  lmmbr  18611  fgcfil  18624  ovolsslem  18770  ovolunlem1  18783  ovoliunnul  18793  itgcn  19124  ellimc3  19156  c1lip3  19273  itgsubstlem  19322  plyss  19508  ulmclm  19693  ulmcau  19699  ulmcn  19703  rlimcxp  20195  chtppilimlem2  20550  chtppilim  20551  isgrpo  20788  opidon  20914  rngmgmbs4  21009  conpcon  23103  cvmliftlem15  23166  cvmlift2lem10  23180  axfelem22  23701  exopcopn  24904  limptlimpr2lem1  24906  tethpnc2  25403  reftr  25621  fnessref  25625  fdc1  25788  sstotbnd3  25832  totbndss  25833  heibor1lem  25865  heibor1  25866  fiphp3d  26234  pell1qrss14  26285  stoweidlem27  27076  stoweidlem35  27084  stoweidlem48  27097  stoweidlem62  27111  lvoli2  28900  paddss2  29137  lhpexle1lem  29326  lhpexle2lem  29328  dvhdimlem  30764  dvh3dim3N  30769  mapdh9a  31110  hdmap11lem2  31165
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-17 1628  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1538  df-nf 1540  df-ral 2520  df-rex 2521
  Copyright terms: Public domain W3C validator