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

Theorem reximdv 2819
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 2818 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1726   E.wrex 2708
This theorem is referenced by:  r19.12  2821  reusv3  4733  iunpw  4761  fvelima  5780  frxp  6458  ssfi  7331  ordtypelem2  7490  wdom2d  7550  xpwdomg  7555  cff1  8140  iunfo  8416  nqereu  8808  reclem3pr  8928  map2psrpr  8987  supsrlem  8988  1re  9092  sswrd  11739  o1lo1  12333  rlimcn1  12384  subcn2  12390  lo1add  12422  lo1mul  12423  pythagtriplem19  13209  vdwnnlem2  13366  ramub2  13384  sylow2alem2  15254  lsmless2x  15281  efgrelexlemb  15384  tgcl  17036  neiss  17175  ssnei2  17182  tgcnp  17319  cnpco  17333  cnpresti  17354  lmcnp  17370  hausnei2  17419  1stcrest  17518  nlly2i  17541  llyss  17544  nllyss  17545  txcnpi  17642  txcmplem1  17675  tx1stc  17684  nrmr0reg  17783  fbssfi  17871  fbfinnfr  17875  fgcl  17912  ufinffr  17963  elfm2  17982  fmfnfmlem1  17988  fmco  17995  fbflim2  18011  flffbas  18029  flftg  18030  cnpflf2  18034  alexsubALT  18084  cnextcn  18100  isucn2  18311  ucnima  18313  blssexps  18458  blssex  18459  mopni3  18526  neibl  18533  metss  18540  metcnp3  18572  cfilucfilOLD  18601  cfilucfil  18602  metustblOLD  18612  metustbl  18613  metutopOLD  18614  psmetutop  18615  rescncf  18929  lebnum  18991  xlebnum  18992  lebnumii  18993  lmmbr  19213  fgcfil  19226  ovolsslem  19382  ovolunlem1  19395  ovoliunnul  19405  itgcn  19736  ellimc3  19768  c1lip3  19885  itgsubstlem  19934  plyss  20120  ulmclm  20305  ulmcau  20313  ulmcn  20317  rlimcxp  20814  chtppilimlem2  21170  chtppilim  21171  usgranloop0  21402  usgra2edg  21404  3v3e3cycl1  21633  4cycl4v4e  21655  4cycl4dv4e  21657  vdusgra0nedg  21681  usgravd0nedg  21685  isgrpo  21786  opidon  21912  rngmgmbs4  22007  tpr2rico  24312  esumpcvgval  24470  conpcon  24924  cvmliftlem15  24987  cvmlift2lem10  25001  reftr  26371  fnessref  26375  fdc1  26452  sstotbnd3  26487  totbndss  26488  heibor1lem  26520  heibor1  26521  fiphp3d  26882  pell1qrss14  26933  infrglb  27700  climrec  27707  stoweidlem27  27754  stoweidlem29  27756  stoweidlem35  27762  stoweidlem48  27775  stoweidlem62  27789  afvelima  28009  exprelprel  28184  3cyclfrgrarn2  28466  vdn0frgrav2  28476  vdgn0frgrav2  28477  frgrawopreg1  28501  frgrawopreg2  28502  lvoli2  30440  paddss2  30677  lhpexle1lem  30866  lhpexle2lem  30868  dvhdimlem  32304  dvh3dim3N  32309  mapdh9a  32650  hdmap11lem2  32705
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2712  df-rex 2713
  Copyright terms: Public domain W3C validator