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

Theorem 2rexbidva 2979
Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 15-Dec-2004.)
Hypothesis
Ref Expression
2rexbidva.1  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  <->  ch )
)
Assertion
Ref Expression
2rexbidva  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  <->  E. x  e.  A  E. y  e.  B  ch )
)
Distinct variable groups:    x, y, ph    y, A
Allowed substitution hints:    ps( x, y)    ch( x, y)    A( x)    B( x, y)

Proof of Theorem 2rexbidva
StepHypRef Expression
1 2rexbidva.1 . . . 4  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  <->  ch )
)
21anassrs 648 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  ( ps 
<->  ch ) )
32rexbidva 2970 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps 
<->  E. y  e.  B  ch ) )
43rexbidva 2970 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  <->  E. x  e.  A  E. y  e.  B  ch )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-rex 2820
This theorem is referenced by:  bezoutlem2  14029  bezoutlem4  14031  vdwmc2  14349  lsmcom2  16468  lsmass  16481  lsmcomx  16652  lsmspsn  17510  hausdiag  19878  imasf1oxms  20724  istrkg2ld  23583  axeuclid  23939  el2wlksot  24553  el2pthsot  24554  usg2spot2nb  24739  shscom  25910  2reu4a  31661  pgrpgt2nabl  32024  3dim0  34253  islpln5  34331  islvol5  34375  isline2  34570  isline3  34572  paddcom  34609  cdlemg2cex  35387
  Copyright terms: Public domain W3C validator