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

Theorem bm1.3ii 4017
Description: Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep 4014. 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 1674 . . . . . . . 8 (𝑥 = 𝑧 → (𝑦𝑥𝑦𝑧))
32imbi2d 229 . . . . . . 7 (𝑥 = 𝑧 → ((𝜑𝑦𝑥) ↔ (𝜑𝑦𝑧)))
43albidv 1778 . . . . . 6 (𝑥 = 𝑧 → (∀𝑦(𝜑𝑦𝑥) ↔ ∀𝑦(𝜑𝑦𝑧)))
54cbvexv 1870 . . . . 5 (∃𝑥𝑦(𝜑𝑦𝑥) ↔ ∃𝑧𝑦(𝜑𝑦𝑧))
61, 5mpbi 144 . . . 4 𝑧𝑦(𝜑𝑦𝑧)
7 ax-sep 4014 . . . 4 𝑥𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))
86, 7pm3.2i 268 . . 3 (∃𝑧𝑦(𝜑𝑦𝑧) ∧ ∃𝑥𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑)))
98exan 1654 . 2 𝑧(∀𝑦(𝜑𝑦𝑧) ∧ ∃𝑥𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑)))
10 19.42v 1860 . . . 4 (∃𝑥(∀𝑦(𝜑𝑦𝑧) ∧ ∀𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))) ↔ (∀𝑦(𝜑𝑦𝑧) ∧ ∃𝑥𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))))
11 bimsc1 930 . . . . . 6 (((𝜑𝑦𝑧) ∧ (𝑦𝑥 ↔ (𝑦𝑧𝜑))) → (𝑦𝑥𝜑))
1211alanimi 1418 . . . . 5 ((∀𝑦(𝜑𝑦𝑧) ∧ ∀𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))) → ∀𝑦(𝑦𝑥𝜑))
1312eximi 1562 . . . 4 (∃𝑥(∀𝑦(𝜑𝑦𝑧) ∧ ∀𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))) → ∃𝑥𝑦(𝑦𝑥𝜑))
1410, 13sylbir 134 . . 3 ((∀𝑦(𝜑𝑦𝑧) ∧ ∃𝑥𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))) → ∃𝑥𝑦(𝑦𝑥𝜑))
1514exlimiv 1560 . 2 (∃𝑧(∀𝑦(𝜑𝑦𝑧) ∧ ∃𝑥𝑦(𝑦𝑥 ↔ (𝑦𝑧𝜑))) → ∃𝑥𝑦(𝑦𝑥𝜑))
169, 15ax-mp 5 1 𝑥𝑦(𝑦𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wal 1312  wex 1451
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-sep 4014
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  axpow3  4069  vpwex  4071  zfpair2  4100  axun2  4325  uniex2  4326
  Copyright terms: Public domain W3C validator