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

Theorem reximdv 2616
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 2615 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 2510
This theorem is referenced by:  r19.12  2618  reusv3  4433  iunpw  4461  fvelima  5426  frxp  6077  ssfi  6968  ordtypelem2  7118  wdom2d  7178  xpwdomg  7183  cff1  7768  iunfo  8045  nqereu  8433  reclem3pr  8553  map2psrpr  8612  supsrlem  8613  1re  8717  sswrd  11300  o1lo1  11888  rlimcn1  11939  subcn2  11945  lo1add  11977  lo1mul  11978  pythagtriplem19  12760  vdwnnlem2  12917  ramub2  12935  sylow2alem2  14764  lsmless2x  14791  efgrelexlemb  14894  tgcl  16539  neiss  16678  ssnei2  16685  tgcnp  16815  cnpco  16828  cnpresti  16848  lmcnp  16864  hausnei2  16913  1stcrest  17011  nlly2i  17034  llyss  17037  nllyss  17038  txcnpi  17134  txcmplem1  17167  tx1stc  17176  nrmr0reg  17272  fbssfi  17364  fbfinnfr  17368  fgcl  17405  ufinffr  17456  elfm2  17475  fmfnfmlem1  17481  fmco  17488  fbflim2  17504  flffbas  17522  flftg  17523  cnpflf2  17527  alexsubALT  17577  blssex  17805  mopni3  17872  neibl  17879  metss  17886  metcnp3  17918  rescncf  18233  lebnum  18294  xlebnum  18295  lebnumii  18296  lmmbr  18516  fgcfil  18529  ovolsslem  18675  ovolunlem1  18688  ovoliunnul  18698  itgcn  19029  ellimc3  19061  c1lip3  19178  itgsubstlem  19227  plyss  19413  ulmclm  19598  ulmcau  19604  ulmcn  19608  rlimcxp  20100  chtppilimlem2  20455  chtppilim  20456  isgrpo  20693  opidon  20819  rngmgmbs4  20914  conpcon  22937  cvmliftlem15  23000  cvmlift2lem10  23014  axfelem22  23535  exopcopn  24738  limptlimpr2lem1  24740  tethpnc2  25237  reftr  25455  fnessref  25459  fdc1  25622  sstotbnd3  25666  totbndss  25667  heibor1lem  25699  heibor1  25700  fiphp3d  26068  pell1qrss14  26119  lvoli2  28529  paddss2  28766  lhpexle1lem  28955  lhpexle2lem  28957  dvhdimlem  30393  dvh3dim3N  30398  mapdh9a  30739  hdmap11lem2  30794
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 2513  df-rex 2514
  Copyright terms: Public domain W3C validator