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

Theorem rexbidv2 2730
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 1637 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  <->  E. x ( x  e.  B  /\  ch ) ) )
3 df-rex 2713 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2713 . 2  |-  ( E. x  e.  B  ch  <->  E. x ( x  e.  B  /\  ch )
)
52, 3, 43bitr4g 281 1  |-  ( ph  ->  ( E. x  e.  A  ps  <->  E. x  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360   E.wex 1551    e. wcel 1726   E.wrex 2708
This theorem is referenced by:  rexss  3412  rexsupp  5857  isoini  6060  exopxfr2  6413  omabs  6892  elfi2  7421  wemapso2lem  7521  ltexpi  8781  rexuz  10529  lpigen  16329  llyi  17539  nllyi  17540  elpi1  19072  xrecex  24168  mrefg2  26763  islssfg2  27148  bnj18eq1  29300  ldual1dim  29966  pmapjat1  30652
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-rex 2713
  Copyright terms: Public domain W3C validator