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

Theorem rexralbidv 2438
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 2414 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32rexbidv 2415 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104  wral 2393  wrex 2394
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-ral 2398  df-rex 2399
This theorem is referenced by:  caucvgpr  7458  caucvgprpr  7488  caucvgsrlemgt1  7571  caucvgsrlemoffres  7576  axcaucvglemres  7675  cvg1nlemres  10725  rexfiuz  10729  resqrexlemgt0  10760  resqrexlemoverl  10761  resqrexlemglsq  10762  resqrexlemsqa  10764  resqrexlemex  10765  cau3lem  10854  caubnd2  10857  climi  11024  2clim  11038  ennnfonelemim  11864  lmcvg  12313  lmss  12342  txlm  12375  metcnpi  12611  metcnpi2  12612  elcncf  12656  cncfi  12661  limcimo  12730  cnplimclemr  12734  limccoap  12743
  Copyright terms: Public domain W3C validator