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

Theorem 2rexbidva 2971
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 646 . . 3  |-  ( ( ( ph  /\  x  e.  A )  /\  y  e.  B )  ->  ( ps 
<->  ch ) )
32rexbidva 2962 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( E. y  e.  B  ps 
<->  E. y  e.  B  ch ) )
43rexbidva 2962 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 367    e. wcel 1823   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-rex 2810
This theorem is referenced by:  bezoutlem2  14261  bezoutlem4  14263  vdwmc2  14581  lsmcom2  16874  lsmass  16887  lsmcomx  17061  lsmspsn  17925  hausdiag  20312  imasf1oxms  21158  istrkg2ld  24056  axeuclid  24468  el2wlksot  25082  el2pthsot  25083  usg2spot2nb  25267  shscom  26435  2reu4a  32433  pgrpgt2nabl  33213  elbigolo1  33432  3dim0  35578  islpln5  35656  islvol5  35700  isline2  35895  isline3  35897  paddcom  35934  cdlemg2cex  36714
  Copyright terms: Public domain W3C validator