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

Theorem rexbidv2 2566
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 1612 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  <->  E. x ( x  e.  B  /\  ch ) ) )
3 df-rex 2549 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2549 . 2  |-  ( E. x  e.  B  ch  <->  E. x ( x  e.  B  /\  ch )
)
52, 3, 43bitr4g 279 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   E.wex 1528    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  rexss  3240  rexsupp  5650  isoini  5835  exopxfr2  6184  omabs  6645  elfi2  7168  wemapso2lem  7265  ltexpi  8526  rexuz  10269  lpigen  16008  llyi  17200  nllyi  17201  elpi1  18543  xrecex  23103  mrefg2  26782  islssfg2  27169  stoweidlem57  27806  bnj18eq1  28959  ldual1dim  29356  pmapjat1  30042
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603
This theorem depends on definitions:  df-bi 177  df-ex 1529  df-rex 2549
  Copyright terms: Public domain W3C validator