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

Theorem 2rexbidv 2392
Description: Formula-building rule for restricted existential quantifiers (deduction rule). (Contributed by NM, 28-Jan-2006.)
Hypothesis
Ref Expression
2ralbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
2rexbidv (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Distinct variable groups:   𝜑,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝜒(𝑥,𝑦)   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)

Proof of Theorem 2rexbidv
StepHypRef Expression
1 2ralbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21rexbidv 2370 . 2 (𝜑 → (∃𝑦𝐵 𝜓 ↔ ∃𝑦𝐵 𝜒))
32rexbidv 2370 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓 ↔ ∃𝑥𝐴𝑦𝐵 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103  wrex 2350
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468
This theorem depends on definitions:  df-bi 115  df-nf 1391  df-rex 2355
This theorem is referenced by:  f1oiso  5496  elrnmpt2g  5644  elrnmpt2  5645  ralrnmpt2  5646  rexrnmpt2  5647  ovelrn  5680  eroveu  6263  genipv  6761  genpelxp  6763  genpelvl  6764  genpelvu  6765  axcnre  7109  apreap  7754  apreim  7770  bezoutlemnewy  10529  bezoutlema  10532  bezoutlemb  10533
  Copyright terms: Public domain W3C validator