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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 ↔ ∀ 𝑧 ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) ) )