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

Theorem rexralbidv 2350
 Description: Formula-building rule for restricted quantifiers (deduction rule). (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 2326 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32rexbidv 2327 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98  ∀wral 2306  ∃wrex 2307 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311  df-rex 2312 This theorem is referenced by:  caucvgpr  6780  caucvgprpr  6810  caucvgsrlemgt1  6879  caucvgsrlemoffres  6884  axcaucvglemres  6973  cvg1nlemres  9584  resqrexlemgt0  9618  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemsqa  9622  resqrexlemex  9623  cau3lem  9710  caubnd2  9713  climi  9808  2clim  9822
 Copyright terms: Public domain W3C validator