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

Theorem rexralbidv 2516
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 2490 . 2 (𝜑 → (∀𝑦𝐵 𝜓 ↔ ∀𝑦𝐵 𝜒))
32rexbidv 2491 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105  wral 2468  wrex 2469
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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473  df-rex 2474
This theorem is referenced by:  caucvgpr  7716  caucvgprpr  7746  caucvgsrlemgt1  7829  caucvgsrlemoffres  7834  axcaucvglemres  7933  cvg1nlemres  11035  rexfiuz  11039  resqrexlemgt0  11070  resqrexlemoverl  11071  resqrexlemglsq  11072  resqrexlemsqa  11074  resqrexlemex  11075  cau3lem  11164  caubnd2  11167  climi  11336  2clim  11350  ennnfonelemim  12486  lmcvg  14202  lmss  14231  txlm  14264  metcnpi  14500  metcnpi2  14501  elcncf  14545  cncfi  14550  limcimo  14619  cnplimclemr  14623  limccoap  14632
  Copyright terms: Public domain W3C validator