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

Theorem rexralbidv 2503
Description: Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2ralbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
rexralbidv  |-  ( ph  ->  ( E. x  e.  A  A. y  e.  B  ps  <->  E. x  e.  A  A. 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 rexralbidv
StepHypRef Expression
1 2ralbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21ralbidv 2477 . 2  |-  ( ph  ->  ( A. y  e.  B  ps  <->  A. y  e.  B  ch )
)
32rexbidv 2478 1  |-  ( ph  ->  ( E. x  e.  A  A. y  e.  B  ps  <->  E. x  e.  A  A. y  e.  B  ch )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 105   A.wral 2455   E.wrex 2456
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461
This theorem is referenced by:  caucvgpr  7659  caucvgprpr  7689  caucvgsrlemgt1  7772  caucvgsrlemoffres  7777  axcaucvglemres  7876  cvg1nlemres  10965  rexfiuz  10969  resqrexlemgt0  11000  resqrexlemoverl  11001  resqrexlemglsq  11002  resqrexlemsqa  11004  resqrexlemex  11005  cau3lem  11094  caubnd2  11097  climi  11266  2clim  11280  ennnfonelemim  12395  lmcvg  13350  lmss  13379  txlm  13412  metcnpi  13648  metcnpi2  13649  elcncf  13693  cncfi  13698  limcimo  13767  cnplimclemr  13771  limccoap  13780
  Copyright terms: Public domain W3C validator