This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pm13.183

Description: Compare theorem *13.183 in WhiteheadRussell p. 178. Only A is required to be a set. (Contributed by Andrew Salmon, 3-Jun-2011) Avoid ax-13 . (Revised by Wolf Lammen, 29-Apr-2023)

Ref Expression
Assertion pm13.183 ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 ↔ ∀ 𝑧 ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ ( 𝑦 = 𝐴 → ( 𝑦 = 𝐵 ↔ 𝐴 = 𝐵 ) )
2 eqeq2 ⊢ ( 𝑦 = 𝐴 → ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐴 ) )
3 2 bibi1d ⊢ ( 𝑦 = 𝐴 → ( ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐵 ) ↔ ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) ) )
4 3 albidv ⊢ ( 𝑦 = 𝐴 → ( ∀ 𝑧 ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐵 ) ↔ ∀ 𝑧 ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) ) )
5 eqeq2 ⊢ ( 𝑦 = 𝐵 → ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐵 ) )
6 5 alrimiv ⊢ ( 𝑦 = 𝐵 → ∀ 𝑧 ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐵 ) )
7 stdpc4 ⊢ ( ∀ 𝑧 ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐵 ) → [ 𝑦 / 𝑧 ] ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐵 ) )
8 sbbi ⊢ ( [ 𝑦 / 𝑧 ] ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐵 ) ↔ ( [ 𝑦 / 𝑧 ] 𝑧 = 𝑦 ↔ [ 𝑦 / 𝑧 ] 𝑧 = 𝐵 ) )
9 equsb1v ⊢ [ 𝑦 / 𝑧 ] 𝑧 = 𝑦
10 9 tbt ⊢ ( [ 𝑦 / 𝑧 ] 𝑧 = 𝐵 ↔ ( [ 𝑦 / 𝑧 ] 𝑧 = 𝐵 ↔ [ 𝑦 / 𝑧 ] 𝑧 = 𝑦 ) )
11 bicom ⊢ ( ( [ 𝑦 / 𝑧 ] 𝑧 = 𝐵 ↔ [ 𝑦 / 𝑧 ] 𝑧 = 𝑦 ) ↔ ( [ 𝑦 / 𝑧 ] 𝑧 = 𝑦 ↔ [ 𝑦 / 𝑧 ] 𝑧 = 𝐵 ) )
12 10 11 bitri ⊢ ( [ 𝑦 / 𝑧 ] 𝑧 = 𝐵 ↔ ( [ 𝑦 / 𝑧 ] 𝑧 = 𝑦 ↔ [ 𝑦 / 𝑧 ] 𝑧 = 𝐵 ) )
13 eqsb1 ⊢ ( [ 𝑦 / 𝑧 ] 𝑧 = 𝐵 ↔ 𝑦 = 𝐵 )
14 8 12 13 3bitr2i ⊢ ( [ 𝑦 / 𝑧 ] ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐵 ) ↔ 𝑦 = 𝐵 )
15 7 14 sylib ⊢ ( ∀ 𝑧 ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐵 ) → 𝑦 = 𝐵 )
16 6 15 impbii ⊢ ( 𝑦 = 𝐵 ↔ ∀ 𝑧 ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐵 ) )
17 1 4 16 vtoclbg ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 ↔ ∀ 𝑧 ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) ) )