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

Theorem 2rexbidva 2756
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 648 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  ( ps 
<->  ch ) )
32rexbidva 2732 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps 
<->  E. y  e.  B  ch ) )
43rexbidva 2732 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 1756   E.wrex 2716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-rex 2721
This theorem is referenced by:  bezoutlem2  13723  bezoutlem4  13725  vdwmc2  14040  lsmcom2  16154  lsmass  16167  lsmcomx  16338  lsmspsn  17165  hausdiag  19218  imasf1oxms  20064  axeuclid  23209  shscom  24722  2reu4a  30013  el2wlksot  30399  el2pthsot  30400  usg2spot2nb  30658  pgrpgt2nabel  30769  3dim0  33101  islpln5  33179  islvol5  33223  isline2  33418  isline3  33420  paddcom  33457  cdlemg2cex  34235
  Copyright terms: Public domain W3C validator