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

Theorem reximdv 2656
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 2655 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1686   E.wrex 2546
This theorem is referenced by:  r19.12  2658  reusv3  4544  iunpw  4572  fvelima  5576  frxp  6227  ssfi  7085  ordtypelem2  7236  wdom2d  7296  xpwdomg  7301  cff1  7886  iunfo  8163  nqereu  8555  reclem3pr  8675  map2psrpr  8734  supsrlem  8735  1re  8839  sswrd  11425  o1lo1  12013  rlimcn1  12064  subcn2  12070  lo1add  12102  lo1mul  12103  pythagtriplem19  12888  vdwnnlem2  13045  ramub2  13063  sylow2alem2  14931  lsmless2x  14958  efgrelexlemb  15061  tgcl  16709  neiss  16848  ssnei2  16855  tgcnp  16985  cnpco  16998  cnpresti  17018  lmcnp  17034  hausnei2  17083  1stcrest  17181  nlly2i  17204  llyss  17207  nllyss  17208  txcnpi  17304  txcmplem1  17337  tx1stc  17346  nrmr0reg  17442  fbssfi  17534  fbfinnfr  17538  fgcl  17575  ufinffr  17626  elfm2  17645  fmfnfmlem1  17651  fmco  17658  fbflim2  17674  flffbas  17692  flftg  17693  cnpflf2  17697  alexsubALT  17747  blssex  17975  mopni3  18042  neibl  18049  metss  18056  metcnp3  18088  rescncf  18403  lebnum  18464  xlebnum  18465  lebnumii  18466  lmmbr  18686  fgcfil  18699  ovolsslem  18845  ovolunlem1  18858  ovoliunnul  18868  itgcn  19199  ellimc3  19231  c1lip3  19348  itgsubstlem  19397  plyss  19583  ulmclm  19768  ulmcau  19774  ulmcn  19778  rlimcxp  20270  chtppilimlem2  20625  chtppilim  20626  isgrpo  20865  opidon  20991  rngmgmbs4  21086  tpr2rico  23298  esumpcvgval  23448  conpcon  23768  cvmliftlem15  23831  cvmlift2lem10  23845  exopcopn  25583  limptlimpr2lem1  25585  tethpnc2  26082  reftr  26300  fnessref  26304  fdc1  26467  sstotbnd3  26511  totbndss  26512  heibor1lem  26544  heibor1  26545  fiphp3d  26913  pell1qrss14  26964  infrglb  27733  stoweidlem27  27787  stoweidlem35  27795  stoweidlem48  27808  stoweidlem62  27822  afvelima  28040  lvoli2  29843  paddss2  30080  lhpexle1lem  30269  lhpexle2lem  30271  dvhdimlem  31707  dvh3dim3N  31712  mapdh9a  32053  hdmap11lem2  32108
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-11 1717
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1531  df-nf 1534  df-ral 2550  df-rex 2551
  Copyright terms: Public domain W3C validator