Metamath Proof Explorer


Theorem bm1.3ii

Description: Convert implication to equivalence using the Separation Scheme (Aussonderung) ax-sep . Similar to Theorem 1.3(ii) of BellMachover p. 463. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypothesis bm1.3ii.1 𝑥𝑦 ( 𝜑𝑦𝑥 )
Assertion bm1.3ii 𝑥𝑦 ( 𝑦𝑥𝜑 )

Proof

Step Hyp Ref Expression
1 bm1.3ii.1 𝑥𝑦 ( 𝜑𝑦𝑥 )
2 19.42v ( ∃ 𝑥 ( ∀ 𝑦 ( 𝜑𝑦𝑧 ) ∧ ∀ 𝑦 ( 𝑦𝑥 ↔ ( 𝑦𝑧𝜑 ) ) ) ↔ ( ∀ 𝑦 ( 𝜑𝑦𝑧 ) ∧ ∃ 𝑥𝑦 ( 𝑦𝑥 ↔ ( 𝑦𝑧𝜑 ) ) ) )
3 bimsc1 ( ( ( 𝜑𝑦𝑧 ) ∧ ( 𝑦𝑥 ↔ ( 𝑦𝑧𝜑 ) ) ) → ( 𝑦𝑥𝜑 ) )
4 3 alanimi ( ( ∀ 𝑦 ( 𝜑𝑦𝑧 ) ∧ ∀ 𝑦 ( 𝑦𝑥 ↔ ( 𝑦𝑧𝜑 ) ) ) → ∀ 𝑦 ( 𝑦𝑥𝜑 ) )
5 4 eximi ( ∃ 𝑥 ( ∀ 𝑦 ( 𝜑𝑦𝑧 ) ∧ ∀ 𝑦 ( 𝑦𝑥 ↔ ( 𝑦𝑧𝜑 ) ) ) → ∃ 𝑥𝑦 ( 𝑦𝑥𝜑 ) )
6 2 5 sylbir ( ( ∀ 𝑦 ( 𝜑𝑦𝑧 ) ∧ ∃ 𝑥𝑦 ( 𝑦𝑥 ↔ ( 𝑦𝑧𝜑 ) ) ) → ∃ 𝑥𝑦 ( 𝑦𝑥𝜑 ) )
7 elequ2 ( 𝑥 = 𝑧 → ( 𝑦𝑥𝑦𝑧 ) )
8 7 imbi2d ( 𝑥 = 𝑧 → ( ( 𝜑𝑦𝑥 ) ↔ ( 𝜑𝑦𝑧 ) ) )
9 8 albidv ( 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝜑𝑦𝑥 ) ↔ ∀ 𝑦 ( 𝜑𝑦𝑧 ) ) )
10 9 cbvexvw ( ∃ 𝑥𝑦 ( 𝜑𝑦𝑥 ) ↔ ∃ 𝑧𝑦 ( 𝜑𝑦𝑧 ) )
11 1 10 mpbi 𝑧𝑦 ( 𝜑𝑦𝑧 )
12 ax-sep 𝑥𝑦 ( 𝑦𝑥 ↔ ( 𝑦𝑧𝜑 ) )
13 11 12 exan 𝑧 ( ∀ 𝑦 ( 𝜑𝑦𝑧 ) ∧ ∃ 𝑥𝑦 ( 𝑦𝑥 ↔ ( 𝑦𝑧𝜑 ) ) )
14 6 13 exlimiiv 𝑥𝑦 ( 𝑦𝑥𝜑 )