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

Theorem rexbidv2 2889
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 1722 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  <->  E. x ( x  e.  B  /\  ch ) ) )
3 df-rex 2738 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2738 . 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 367   E.wex 1620    e. wcel 1826   E.wrex 2733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712
This theorem depends on definitions:  df-bi 185  df-ex 1621  df-rex 2738
This theorem is referenced by:  rexbidva  2890  rexss  3481  exopxfr2  5060  rexsuppOLD  5914  isoini  6135  rexsupp  6836  omabs  7214  elfi2  7789  wemapsolem  7890  ltexpi  9191  rexuz  11051  lpigen  18017  llyi  20060  nllyi  20061  elpi1  21630  xrecex  27769  mrefg2  30805  islssfg2  31183  fourierdlem71  32126  bnj18eq1  34332  ldual1dim  35304  pmapjat1  35990
  Copyright terms: Public domain W3C validator