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

Theorem reximdv 2629
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 2628 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 2519
This theorem is referenced by:  r19.12  2631  reusv3  4514  iunpw  4542  fvelima  5508  frxp  6159  ssfi  7051  ordtypelem2  7202  wdom2d  7262  xpwdomg  7267  cff1  7852  iunfo  8129  nqereu  8521  reclem3pr  8641  map2psrpr  8700  supsrlem  8701  1re  8805  sswrd  11389  o1lo1  11977  rlimcn1  12028  subcn2  12034  lo1add  12066  lo1mul  12067  pythagtriplem19  12849  vdwnnlem2  13006  ramub2  13024  sylow2alem2  14892  lsmless2x  14919  efgrelexlemb  15022  tgcl  16670  neiss  16809  ssnei2  16816  tgcnp  16946  cnpco  16959  cnpresti  16979  lmcnp  16995  hausnei2  17044  1stcrest  17142  nlly2i  17165  llyss  17168  nllyss  17169  txcnpi  17265  txcmplem1  17298  tx1stc  17307  nrmr0reg  17403  fbssfi  17495  fbfinnfr  17499  fgcl  17536  ufinffr  17587  elfm2  17606  fmfnfmlem1  17612  fmco  17619  fbflim2  17635  flffbas  17653  flftg  17654  cnpflf2  17658  alexsubALT  17708  blssex  17936  mopni3  18003  neibl  18010  metss  18017  metcnp3  18049  rescncf  18364  lebnum  18425  xlebnum  18426  lebnumii  18427  lmmbr  18647  fgcfil  18660  ovolsslem  18806  ovolunlem1  18819  ovoliunnul  18829  itgcn  19160  ellimc3  19192  c1lip3  19309  itgsubstlem  19358  plyss  19544  ulmclm  19729  ulmcau  19735  ulmcn  19739  rlimcxp  20231  chtppilimlem2  20586  chtppilim  20587  isgrpo  20824  opidon  20950  rngmgmbs4  21045  conpcon  23139  cvmliftlem15  23202  cvmlift2lem10  23216  axfelem22  23737  exopcopn  24940  limptlimpr2lem1  24942  tethpnc2  25439  reftr  25657  fnessref  25661  fdc1  25824  sstotbnd3  25868  totbndss  25869  heibor1lem  25901  heibor1  25902  fiphp3d  26270  pell1qrss14  26321  infrglb  27091  stoweidlem27  27145  stoweidlem35  27153  stoweidlem48  27166  stoweidlem62  27180  lvoli2  29020  paddss2  29257  lhpexle1lem  29446  lhpexle2lem  29448  dvhdimlem  30884  dvh3dim3N  30889  mapdh9a  31230  hdmap11lem2  31285
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 2523  df-rex 2524
  Copyright terms: Public domain W3C validator