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

Theorem rexbidv2 2868
Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
rexbidv2.1  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  B  /\  ch ) ) )
Assertion
Ref Expression
rexbidv2  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ch )
)
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)    B( x)

Proof of Theorem rexbidv2
StepHypRef Expression
1 rexbidv2.1 . . 3  |-  ( ph  ->  ( ( x  e.  A  /\  ps )  <->  ( x  e.  B  /\  ch ) ) )
21exbidv 1681 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  <->  E. x ( x  e.  B  /\  ch ) ) )
3 df-rex 2804 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2804 . 2  |-  ( E. x  e.  B  ch  <->  E. x ( x  e.  B  /\  ch )
)
52, 3, 43bitr4g 288 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   E.wex 1587    e. wcel 1758   E.wrex 2799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-rex 2804
This theorem is referenced by:  rexss  3526  exopxfr2  5091  rexsuppOLD  5936  isoini  6137  rexsupp  6816  omabs  7195  elfi2  7774  wemapsolem  7874  ltexpi  9181  rexuz  11015  lpigen  17460  llyi  19209  nllyi  19210  elpi1  20748  xrecex  26239  mrefg2  29190  islssfg2  29571  bnj18eq1  32237  ldual1dim  33134  pmapjat1  33820
  Copyright terms: Public domain W3C validator