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

Theorem reximdv 2654
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 2653 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  r19.12  2656  reusv3  4542  iunpw  4570  fvelima  5574  frxp  6225  ssfi  7083  ordtypelem2  7234  wdom2d  7294  xpwdomg  7299  cff1  7884  iunfo  8161  nqereu  8553  reclem3pr  8673  map2psrpr  8732  supsrlem  8733  1re  8837  sswrd  11423  o1lo1  12011  rlimcn1  12062  subcn2  12068  lo1add  12100  lo1mul  12101  pythagtriplem19  12886  vdwnnlem2  13043  ramub2  13061  sylow2alem2  14929  lsmless2x  14956  efgrelexlemb  15059  tgcl  16707  neiss  16846  ssnei2  16853  tgcnp  16983  cnpco  16996  cnpresti  17016  lmcnp  17032  hausnei2  17081  1stcrest  17179  nlly2i  17202  llyss  17205  nllyss  17206  txcnpi  17302  txcmplem1  17335  tx1stc  17344  nrmr0reg  17440  fbssfi  17532  fbfinnfr  17536  fgcl  17573  ufinffr  17624  elfm2  17643  fmfnfmlem1  17649  fmco  17656  fbflim2  17672  flffbas  17690  flftg  17691  cnpflf2  17695  alexsubALT  17745  blssex  17973  mopni3  18040  neibl  18047  metss  18054  metcnp3  18086  rescncf  18401  lebnum  18462  xlebnum  18463  lebnumii  18464  lmmbr  18684  fgcfil  18697  ovolsslem  18843  ovolunlem1  18856  ovoliunnul  18866  itgcn  19197  ellimc3  19229  c1lip3  19346  itgsubstlem  19395  plyss  19581  ulmclm  19766  ulmcau  19772  ulmcn  19776  rlimcxp  20268  chtppilimlem2  20623  chtppilim  20624  isgrpo  20863  opidon  20989  rngmgmbs4  21084  tpr2rico  23296  esumpcvgval  23446  conpcon  23766  cvmliftlem15  23829  cvmlift2lem10  23843  exopcopn  25572  limptlimpr2lem1  25574  tethpnc2  26071  reftr  26289  fnessref  26293  fdc1  26456  sstotbnd3  26500  totbndss  26501  heibor1lem  26533  heibor1  26534  fiphp3d  26902  pell1qrss14  26953  infrglb  27722  stoweidlem27  27776  stoweidlem35  27784  stoweidlem48  27797  stoweidlem62  27811  afvelima  28029  lvoli2  29770  paddss2  30007  lhpexle1lem  30196  lhpexle2lem  30198  dvhdimlem  31634  dvh3dim3N  31639  mapdh9a  31980  hdmap11lem2  32035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2548  df-rex 2549
  Copyright terms: Public domain W3C validator