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

Theorem reximdv 2781
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 2780 1  |-  ( ph  ->  ( E. x  e.  A  ps  ->  E. x  e.  A  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   E.wrex 2671
This theorem is referenced by:  r19.12  2783  reusv3  4694  iunpw  4722  fvelima  5741  frxp  6419  ssfi  7292  ordtypelem2  7448  wdom2d  7508  xpwdomg  7513  cff1  8098  iunfo  8374  nqereu  8766  reclem3pr  8886  map2psrpr  8945  supsrlem  8946  1re  9050  sswrd  11696  o1lo1  12290  rlimcn1  12341  subcn2  12347  lo1add  12379  lo1mul  12380  pythagtriplem19  13166  vdwnnlem2  13323  ramub2  13341  sylow2alem2  15211  lsmless2x  15238  efgrelexlemb  15341  tgcl  16993  neiss  17132  ssnei2  17139  tgcnp  17275  cnpco  17289  cnpresti  17310  lmcnp  17326  hausnei2  17375  1stcrest  17473  nlly2i  17496  llyss  17499  nllyss  17500  txcnpi  17597  txcmplem1  17630  tx1stc  17639  nrmr0reg  17738  fbssfi  17826  fbfinnfr  17830  fgcl  17867  ufinffr  17918  elfm2  17937  fmfnfmlem1  17943  fmco  17950  fbflim2  17966  flffbas  17984  flftg  17985  cnpflf2  17989  alexsubALT  18039  cnextcn  18055  isucn2  18266  ucnima  18268  blssexps  18413  blssex  18414  mopni3  18481  neibl  18488  metss  18495  metcnp3  18527  cfilucfilOLD  18556  cfilucfil  18557  metustblOLD  18567  metustbl  18568  metutopOLD  18569  psmetutop  18570  rescncf  18884  lebnum  18946  xlebnum  18947  lebnumii  18948  lmmbr  19168  fgcfil  19181  ovolsslem  19337  ovolunlem1  19350  ovoliunnul  19360  itgcn  19691  ellimc3  19723  c1lip3  19840  itgsubstlem  19889  plyss  20075  ulmclm  20260  ulmcau  20268  ulmcn  20272  rlimcxp  20769  chtppilimlem2  21125  chtppilim  21126  usgranloop0  21357  usgra2edg  21359  3v3e3cycl1  21588  4cycl4v4e  21610  4cycl4dv4e  21612  vdusgra0nedg  21636  usgravd0nedg  21640  isgrpo  21741  opidon  21867  rngmgmbs4  21962  tpr2rico  24267  esumpcvgval  24425  conpcon  24879  cvmliftlem15  24942  cvmlift2lem10  24956  reftr  26263  fnessref  26267  fdc1  26344  sstotbnd3  26379  totbndss  26380  heibor1lem  26412  heibor1  26413  fiphp3d  26774  pell1qrss14  26825  infrglb  27593  climrec  27600  stoweidlem27  27647  stoweidlem29  27649  stoweidlem35  27655  stoweidlem48  27668  stoweidlem62  27682  afvelima  27902  3cyclfrgrarn2  28122  vdn0frgrav2  28132  vdgn0frgrav2  28133  frgrawopreg1  28157  frgrawopreg2  28158  lvoli2  30067  paddss2  30304  lhpexle1lem  30493  lhpexle2lem  30495  dvhdimlem  31931  dvh3dim3N  31936  mapdh9a  32277  hdmap11lem2  32332
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 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2675  df-rex 2676
  Copyright terms: Public domain W3C validator