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

Theorem rexralbidv 2464
 Description: Formula-building rule for restricted quantifiers (deduction form). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2ralbidv.1
Assertion
Ref Expression
rexralbidv
Distinct variable groups:   ,   ,
Allowed substitution hints:   (,)   (,)   (,)   (,)

Proof of Theorem rexralbidv
StepHypRef Expression
1 2ralbidv.1 . . 3
21ralbidv 2438 . 2
32rexbidv 2439 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 104  wral 2417  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-ral 2422  df-rex 2423 This theorem is referenced by:  caucvgpr  7515  caucvgprpr  7545  caucvgsrlemgt1  7628  caucvgsrlemoffres  7633  axcaucvglemres  7732  cvg1nlemres  10790  rexfiuz  10794  resqrexlemgt0  10825  resqrexlemoverl  10826  resqrexlemglsq  10827  resqrexlemsqa  10829  resqrexlemex  10830  cau3lem  10919  caubnd2  10922  climi  11089  2clim  11103  ennnfonelemim  11974  lmcvg  12426  lmss  12455  txlm  12488  metcnpi  12724  metcnpi2  12725  elcncf  12769  cncfi  12774  limcimo  12843  cnplimclemr  12847  limccoap  12856
 Copyright terms: Public domain W3C validator