Metamath Proof Explorer


Theorem bj-sb

Description: A weak variant of sbid2 not requiring ax-13 nor ax-10 . On top of Tarski's FOL, one implication requires only ax12v , and the other requires only sp . (Contributed by BJ, 25-May-2021)

Ref Expression
Assertion bj-sb ( 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 ax12v ( 𝑥 = 𝑦 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )
2 1 equcoms ( 𝑦 = 𝑥 → ( 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )
3 2 com12 ( 𝜑 → ( 𝑦 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )
4 3 alrimiv ( 𝜑 → ∀ 𝑦 ( 𝑦 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )
5 sp ( ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) → ( 𝑥 = 𝑦𝜑 ) )
6 5 com12 ( 𝑥 = 𝑦 → ( ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) → 𝜑 ) )
7 6 equcoms ( 𝑦 = 𝑥 → ( ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) → 𝜑 ) )
8 7 a2i ( ( 𝑦 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) → ( 𝑦 = 𝑥𝜑 ) )
9 8 alimi ( ∀ 𝑦 ( 𝑦 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) → ∀ 𝑦 ( 𝑦 = 𝑥𝜑 ) )
10 bj-eqs ( 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑥𝜑 ) )
11 9 10 sylibr ( ∀ 𝑦 ( 𝑦 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) → 𝜑 )
12 4 11 impbii ( 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) ) )