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

Theorem reubidv 3051
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 17-Oct-1996.)
Hypothesis
Ref Expression
reubidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
reubidv  |-  ( 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 reubidv
StepHypRef Expression
1 reubidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21adantr 465 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
32reubidva 3050 1  |-  ( ph  ->  ( E! x  e.  A  ps  <->  E! x  e.  A  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    e. wcel 1767   E!wreu 2819
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-eu 2279  df-reu 2824
This theorem is referenced by:  reueqd  3073  sbcreu  3423  sbcreugOLD  3424  reusv6OLD  4664  reusv7OLD  4665  oawordeu  7216  xpf1o  7691  dfac2  8523  creur  10542  creui  10543  divalg  13937  divalg2  13939  lubfval  15482  lubeldm  15485  lubval  15488  glbfval  15495  glbeldm  15498  glbval  15501  joineu  15514  meeteu  15528  dfod2  16459  ustuqtop  20617  isfrgra  24804  frgraunss  24809  frgra1v  24812  frgra2v  24813  frgra3v  24816  3vfriswmgra  24819  n4cyclfrgra  24832  riesz4  26797  cnlnadjeu  26811  hdmap1eulem  36977  hdmap1eulemOLDN  36978  hdmap14lem6  37029
  Copyright terms: Public domain W3C validator