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

Theorem 2rexbidva 2597
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 2573 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps 
<->  E. y  e.  B  ch ) )
43rexbidva 2573 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 1696   E.wrex 2557
This theorem is referenced by:  bezoutlem2  12734  bezoutlem4  12736  vdwmc2  13042  lsmcom2  14982  lsmass  14995  lsmcomx  15164  lsmspsn  15853  hausdiag  17355  imasf1oxms  18051  shscom  21914  axeuclid  24663  2reu4a  28070  3dim0  30268  islpln5  30346  islvol5  30390  isline2  30585  isline3  30587  paddcom  30624  cdlemg2cex  31402
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  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535  df-rex 2562
  Copyright terms: Public domain W3C validator