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

Theorem reximdv 2655
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 2654 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1685   E.wrex 2545
This theorem is referenced by:  r19.12  2657  reusv3  4541  iunpw  4569  fvelima  5536  frxp  6187  ssfi  7079  ordtypelem2  7230  wdom2d  7290  xpwdomg  7295  cff1  7880  iunfo  8157  nqereu  8549  reclem3pr  8669  map2psrpr  8728  supsrlem  8729  1re  8833  sswrd  11419  o1lo1  12007  rlimcn1  12058  subcn2  12064  lo1add  12096  lo1mul  12097  pythagtriplem19  12882  vdwnnlem2  13039  ramub2  13057  sylow2alem2  14925  lsmless2x  14952  efgrelexlemb  15055  tgcl  16703  neiss  16842  ssnei2  16849  tgcnp  16979  cnpco  16992  cnpresti  17012  lmcnp  17028  hausnei2  17077  1stcrest  17175  nlly2i  17198  llyss  17201  nllyss  17202  txcnpi  17298  txcmplem1  17331  tx1stc  17340  nrmr0reg  17436  fbssfi  17528  fbfinnfr  17532  fgcl  17569  ufinffr  17620  elfm2  17639  fmfnfmlem1  17645  fmco  17652  fbflim2  17668  flffbas  17686  flftg  17687  cnpflf2  17691  alexsubALT  17741  blssex  17969  mopni3  18036  neibl  18043  metss  18050  metcnp3  18082  rescncf  18397  lebnum  18458  xlebnum  18459  lebnumii  18460  lmmbr  18680  fgcfil  18693  ovolsslem  18839  ovolunlem1  18852  ovoliunnul  18862  itgcn  19193  ellimc3  19225  c1lip3  19342  itgsubstlem  19391  plyss  19577  ulmclm  19762  ulmcau  19768  ulmcn  19772  rlimcxp  20264  chtppilimlem2  20619  chtppilim  20620  isgrpo  20857  opidon  20983  rngmgmbs4  21078  conpcon  23173  cvmliftlem15  23236  cvmlift2lem10  23250  axfelem22  23771  exopcopn  24983  limptlimpr2lem1  24985  tethpnc2  25482  reftr  25700  fnessref  25704  fdc1  25867  sstotbnd3  25911  totbndss  25912  heibor1lem  25944  heibor1  25945  fiphp3d  26313  pell1qrss14  26364  infrglb  27133  stoweidlem27  27187  stoweidlem35  27195  stoweidlem48  27208  stoweidlem62  27222  afvelima  27420  lvoli2  29049  paddss2  29286  lhpexle1lem  29475  lhpexle2lem  29477  dvhdimlem  30913  dvh3dim3N  30918  mapdh9a  31259  hdmap11lem2  31314
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 1636  ax-8 1644  ax-11 1716
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-ral 2549  df-rex 2550
  Copyright terms: Public domain W3C validator