Metamath Proof Explorer


Theorem bj-ssblem2

Description: An instance of ax-11 proved without it. The converse may not be provable without ax-11 (since using alcomiw would require a DV on ph , x , which defeats the purpose). (Contributed by BJ, 22-Dec-2020) (Proof modification is discouraged.)

Ref Expression
Assertion bj-ssblem2 ( ∀ 𝑥𝑦 ( 𝑦 = 𝑡 → ( 𝑥 = 𝑦𝜑 ) ) → ∀ 𝑦𝑥 ( 𝑦 = 𝑡 → ( 𝑥 = 𝑦𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 equequ1 ( 𝑦 = 𝑧 → ( 𝑦 = 𝑡𝑧 = 𝑡 ) )
2 equequ2 ( 𝑦 = 𝑧 → ( 𝑥 = 𝑦𝑥 = 𝑧 ) )
3 2 imbi1d ( 𝑦 = 𝑧 → ( ( 𝑥 = 𝑦𝜑 ) ↔ ( 𝑥 = 𝑧𝜑 ) ) )
4 1 3 imbi12d ( 𝑦 = 𝑧 → ( ( 𝑦 = 𝑡 → ( 𝑥 = 𝑦𝜑 ) ) ↔ ( 𝑧 = 𝑡 → ( 𝑥 = 𝑧𝜑 ) ) ) )
5 4 alcomiw ( ∀ 𝑥𝑦 ( 𝑦 = 𝑡 → ( 𝑥 = 𝑦𝜑 ) ) → ∀ 𝑦𝑥 ( 𝑦 = 𝑡 → ( 𝑥 = 𝑦𝜑 ) ) )