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

Theorem bm1.3ii 4019
Description: Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4016. Similar to Theorem 1.3ii of [BellMachover] p. 463. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
bm1.3ii.1 𝑥𝑦(𝜑𝑦𝑥)
Assertion
Ref Expression
bm1.3ii 𝑥𝑦(𝑦𝑥𝜑)
Distinct variable groups:   𝜑,𝑥   𝑥,𝑦
Allowed substitution hint:   𝜑(𝑦)

Proof of Theorem bm1.3ii
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 bm1.3ii.1 . . . . 5 𝑥𝑦(𝜑𝑦𝑥)
2 elequ2 1676 . . . . . . . 8 (𝑥 = 𝑧 → (𝑦𝑥𝑦𝑧))
32imbi2d 229 . . . . . . 7 (𝑥 = 𝑧 → ((𝜑𝑦𝑥) ↔ (𝜑𝑦𝑧)))
43albidv 1780 . . . . . 6 (𝑥 = 𝑧 → (∀𝑦(𝜑𝑦𝑥) ↔ ∀𝑦(𝜑𝑦𝑧)))
54cbvexv 1872 . . . . 5 (∃𝑥𝑦(𝜑𝑦𝑥) ↔ ∃𝑧𝑦(𝜑𝑦𝑧))
61, 5mpbi 144 . . . 4 𝑧𝑦(𝜑𝑦𝑧)
7 ax-sep 4016 . . . 4 𝑥𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))
86, 7pm3.2i 270 . . 3 (∃𝑧𝑦(𝜑𝑦𝑧) ∧ ∃𝑥𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑)))
98exan 1656 . 2 𝑧(∀𝑦(𝜑𝑦𝑧) ∧ ∃𝑥𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑)))
10 19.42v 1862 . . . 4 (∃𝑥(∀𝑦(𝜑𝑦𝑧) ∧ ∀𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))) ↔ (∀𝑦(𝜑𝑦𝑧) ∧ ∃𝑥𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))))
11 bimsc1 932 . . . . . 6 (((𝜑𝑦𝑧) ∧ (𝑦𝑥 ↔ (𝑦𝑧𝜑))) → (𝑦𝑥𝜑))
1211alanimi 1420 . . . . 5 ((∀𝑦(𝜑𝑦𝑧) ∧ ∀𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))) → ∀𝑦(𝑦𝑥𝜑))
1312eximi 1564 . . . 4 (∃𝑥(∀𝑦(𝜑𝑦𝑧) ∧ ∀𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))) → ∃𝑥𝑦(𝑦𝑥𝜑))
1410, 13sylbir 134 . . 3 ((∀𝑦(𝜑𝑦𝑧) ∧ ∃𝑥𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))) → ∃𝑥𝑦(𝑦𝑥𝜑))
1514exlimiv 1562 . 2 (∃𝑧(∀𝑦(𝜑𝑦𝑧) ∧ ∃𝑥𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))) → ∃𝑥𝑦(𝑦𝑥𝜑))
169, 15ax-mp 5 1 𝑥𝑦(𝑦𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wal 1314  wex 1453
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-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-4 1472  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-sep 4016
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  axpow3  4071  vpwex  4073  zfpair2  4102  axun2  4327  uniex2  4328
  Copyright terms: Public domain W3C validator