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

Theorem reubidv 3028
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 3027 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 1804   E!wreu 2795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-12 1840
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-nf 1604  df-eu 2272  df-reu 2800
This theorem is referenced by:  reueqd  3050  sbcreu  3400  sbcreugOLD  3401  reusv6OLD  4648  reusv7OLD  4649  oawordeu  7206  xpf1o  7681  dfac2  8514  creur  10536  creui  10537  divalg  13938  divalg2  13940  lubfval  15482  lubeldm  15485  lubval  15488  glbfval  15495  glbeldm  15498  glbval  15501  joineu  15514  meeteu  15528  dfod2  16460  ustuqtop  20622  isfrgra  24862  frgraunss  24867  frgra1v  24870  frgra2v  24871  frgra3v  24874  3vfriswmgra  24877  n4cyclfrgra  24890  riesz4  26855  cnlnadjeu  26869  hdmap1eulem  37285  hdmap1eulemOLDN  37286  hdmap14lem6  37337
  Copyright terms: Public domain W3C validator