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

Theorem 2rexbidva 2584
Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 15-Dec-2004.)
Hypothesis
Ref Expression
2ralbidva.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 2ralbidva.1 . . . 4  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  -> 
( ps  <->  ch )
)
21anassrs 629 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  ( ps 
<->  ch ) )
32rexbidva 2560 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps 
<->  E. y  e.  B  ch ) )
43rexbidva 2560 1  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  <->  E. x  e.  A  E. y  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  bezoutlem2  12718  bezoutlem4  12720  vdwmc2  13026  lsmcom2  14966  lsmass  14979  lsmcomx  15148  lsmspsn  15837  hausdiag  17339  imasf1oxms  18035  shscom  21898  axeuclid  24591  2reu4a  27967  3dim0  29646  islpln5  29724  islvol5  29768  isline2  29963  isline3  29965  paddcom  30002  cdlemg2cex  30780
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  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-rex 2549
  Copyright terms: Public domain W3C validator