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

Theorem reubidv 2910
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 2909 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 1756   E!wreu 2722
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-eu 2257  df-reu 2727
This theorem is referenced by:  reueqd  2932  sbcreu  3278  sbcreugOLD  3279  reusv6OLD  4508  reusv7OLD  4509  oawordeu  6999  xpf1o  7478  dfac2  8305  creur  10321  creui  10322  divalg  13612  divalg2  13614  lubfval  15153  lubeldm  15156  lubval  15159  glbfval  15166  glbeldm  15169  glbval  15172  joineu  15185  meeteu  15199  dfod2  16070  ustuqtop  19826  riesz4  25473  cnlnadjeu  25487  isfrgra  30587  frgraunss  30592  frgra1v  30595  frgra2v  30596  frgra3v  30599  3vfriswmgra  30602  n4cyclfrgra  30615  hdmap1eulem  35474  hdmap1eulemOLDN  35475  hdmap14lem6  35526
  Copyright terms: Public domain W3C validator