ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  2rexbidv Unicode version

Theorem 2rexbidv 2515
Description: Formula-building rule for restricted existential quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2ralbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
2rexbidv  |-  ( ph  ->  ( E. x  e.  A  E. y  e.  B  ps  <->  E. x  e.  A  E. y  e.  B  ch )
)
Distinct variable groups:    ph, x    ph, y
Allowed substitution hints:    ps( x, y)    ch( x, y)    A( x, y)    B( x, y)

Proof of Theorem 2rexbidv
StepHypRef Expression
1 2ralbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21rexbidv 2491 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2491 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 105   E.wrex 2469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-rex 2474
This theorem is referenced by:  f1oiso  5848  elrnmpog  6010  elrnmpo  6011  ralrnmpo  6012  rexrnmpo  6013  ovelrn  6046  eroveu  6653  genipv  7539  genpelxp  7541  genpelvl  7542  genpelvu  7543  axcnre  7911  apreap  8575  apreim  8591  aprcl  8634  aptap  8638  bezoutlemnewy  12032  bezoutlema  12035  bezoutlemb  12036  pythagtriplem19  12317  pceu  12330  pcval  12331  pczpre  12332  pcdiv  12337  4sqlem2  12424  4sqlem3  12425  4sqlem4  12427  4sqexercise2  12434  4sqlemsdc  12435  4sq  12445  txuni2  14233  txbas  14235  txdis1cn  14255  2sqlem2  14940  2sqlem8  14948  2sqlem9  14949
  Copyright terms: Public domain W3C validator