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		eqsb1	⊢ ( [ 𝑦 / 𝑧 ] 𝑧 = 𝐵 ↔ 𝑦 = 𝐵 )
10	9	bibi2i	⊢ ( ( [ 𝑦 / 𝑧 ] 𝑧 = 𝑦 ↔ [ 𝑦 / 𝑧 ] 𝑧 = 𝐵 ) ↔ ( [ 𝑦 / 𝑧 ] 𝑧 = 𝑦 ↔ 𝑦 = 𝐵 ) )
11		equsb1v	⊢ [ 𝑦 / 𝑧 ] 𝑧 = 𝑦
12		biimp	⊢ ( ( [ 𝑦 / 𝑧 ] 𝑧 = 𝑦 ↔ 𝑦 = 𝐵 ) → ( [ 𝑦 / 𝑧 ] 𝑧 = 𝑦 → 𝑦 = 𝐵 ) )
13	11 12	mpi	⊢ ( ( [ 𝑦 / 𝑧 ] 𝑧 = 𝑦 ↔ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
14	10 13	sylbi	⊢ ( ( [ 𝑦 / 𝑧 ] 𝑧 = 𝑦 ↔ [ 𝑦 / 𝑧 ] 𝑧 = 𝐵 ) → 𝑦 = 𝐵 )
15	8 14	sylbi	⊢ ( [ 𝑦 / 𝑧 ] ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐵 ) → 𝑦 = 𝐵 )
16	7 15	syl	⊢ ( ∀ 𝑧 ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐵 ) → 𝑦 = 𝐵 )
17	6 16	impbii	⊢ ( 𝑦 = 𝐵 ↔ ∀ 𝑧 ( 𝑧 = 𝑦 ↔ 𝑧 = 𝐵 ) )
18	1 4 17	vtoclbg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 ↔ ∀ 𝑧 ( 𝑧 = 𝐴 ↔ 𝑧 = 𝐵 ) ) )