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

Theorem 2rexbidv 2463
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 2439 . 2  |-  ( ph  ->  ( E. y  e.  B  ps  <->  E. y  e.  B  ch )
)
32rexbidv 2439 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 104   E.wrex 2418
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-rex 2423
This theorem is referenced by:  f1oiso  5734  elrnmpog  5890  elrnmpo  5891  ralrnmpo  5892  rexrnmpo  5893  ovelrn  5926  eroveu  6527  genipv  7340  genpelxp  7342  genpelvl  7343  genpelvu  7344  axcnre  7712  apreap  8372  apreim  8388  aprcl  8431  bezoutlemnewy  11718  bezoutlema  11721  bezoutlemb  11722  txuni2  12462  txbas  12464  txdis1cn  12484
  Copyright terms: Public domain W3C validator