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

Theorem rexbidv2 2579
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 1616 . 2  |-  ( ph  ->  ( E. x ( x  e.  A  /\  ps )  <->  E. x ( x  e.  B  /\  ch ) ) )
3 df-rex 2562 . 2  |-  ( E. x  e.  A  ps  <->  E. x ( x  e.  A  /\  ps )
)
4 df-rex 2562 . 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 1531    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  rexss  3253  rexsupp  5666  isoini  5851  exopxfr2  6200  omabs  6661  elfi2  7184  wemapso2lem  7281  ltexpi  8542  rexuz  10285  lpigen  16024  llyi  17216  nllyi  17217  elpi1  18559  xrecex  23119  mrefg2  26885  islssfg2  27272  stoweidlem57  27909  bnj18eq1  29275  ldual1dim  29978  pmapjat1  30664
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606
This theorem depends on definitions:  df-bi 177  df-ex 1532  df-rex 2562
  Copyright terms: Public domain W3C validator