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

Theorem reximdv 2760
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 23 . 2  |-  ( ph  ->  ( x  e.  A  ->  ( ps  ->  ch ) ) )
32reximdvai 2759 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1717   E.wrex 2650
This theorem is referenced by:  r19.12  2762  reusv3  4671  iunpw  4699  fvelima  5717  frxp  6392  ssfi  7265  ordtypelem2  7421  wdom2d  7481  xpwdomg  7486  cff1  8071  iunfo  8347  nqereu  8739  reclem3pr  8859  map2psrpr  8918  supsrlem  8919  1re  9023  sswrd  11664  o1lo1  12258  rlimcn1  12309  subcn2  12315  lo1add  12347  lo1mul  12348  pythagtriplem19  13134  vdwnnlem2  13291  ramub2  13309  sylow2alem2  15179  lsmless2x  15206  efgrelexlemb  15309  tgcl  16957  neiss  17096  ssnei2  17103  tgcnp  17239  cnpco  17253  cnpresti  17274  lmcnp  17290  hausnei2  17339  1stcrest  17437  nlly2i  17460  llyss  17463  nllyss  17464  txcnpi  17561  txcmplem1  17594  tx1stc  17603  nrmr0reg  17702  fbssfi  17790  fbfinnfr  17794  fgcl  17831  ufinffr  17882  elfm2  17901  fmfnfmlem1  17907  fmco  17914  fbflim2  17930  flffbas  17948  flftg  17949  cnpflf2  17953  alexsubALT  18003  cnextcn  18019  isucn2  18230  ucnima  18232  blssex  18347  mopni3  18414  neibl  18421  metss  18428  metcnp3  18460  cfilucfil  18479  metustbl  18486  metutop  18487  rescncf  18798  lebnum  18860  xlebnum  18861  lebnumii  18862  lmmbr  19082  fgcfil  19095  ovolsslem  19247  ovolunlem1  19260  ovoliunnul  19270  itgcn  19601  ellimc3  19633  c1lip3  19750  itgsubstlem  19799  plyss  19985  ulmclm  20170  ulmcau  20178  ulmcn  20182  rlimcxp  20679  chtppilimlem2  21035  chtppilim  21036  usgranloop0  21266  usgra2edg  21268  3v3e3cycl1  21479  4cycl4v4e  21501  4cycl4dv4e  21503  vdusgra0nedg  21527  usgravd0nedg  21531  isgrpo  21632  opidon  21758  rngmgmbs4  21853  tpr2rico  24114  esumpcvgval  24264  conpcon  24701  cvmliftlem15  24764  cvmlift2lem10  24778  reftr  26060  fnessref  26064  fdc1  26141  sstotbnd3  26176  totbndss  26177  heibor1lem  26209  heibor1  26210  fiphp3d  26571  pell1qrss14  26622  infrglb  27390  climrec  27397  stoweidlem27  27444  stoweidlem29  27446  stoweidlem35  27452  stoweidlem48  27465  stoweidlem62  27479  afvelima  27700  3cyclfrgrarn2  27767  vdn0frgrav2  27777  vdgn0frgrav2  27778  frgrawopreg1  27802  frgrawopreg2  27803  lvoli2  29695  paddss2  29932  lhpexle1lem  30121  lhpexle2lem  30123  dvhdimlem  31559  dvh3dim3N  31564  mapdh9a  31905  hdmap11lem2  31960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2654  df-rex 2655
  Copyright terms: Public domain W3C validator