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 ⊢ A ∈ V → A = B ↔ ∀ z z = A ↔ z = B

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ y = A → y = B ↔ A = B
2 eqeq2 ⊢ y = A → z = y ↔ z = A
3 2 bibi1d ⊢ y = A → z = y ↔ z = B ↔ z = A ↔ z = B
4 3 albidv ⊢ y = A → ∀ z z = y ↔ z = B ↔ ∀ z z = A ↔ z = B
5 eqeq2 ⊢ y = B → z = y ↔ z = B
6 5 alrimiv ⊢ y = B → ∀ z z = y ↔ z = B
7 stdpc4 ⊢ ∀ z z = y ↔ z = B → y z z = y ↔ z = B
8 sbbi ⊢ y z z = y ↔ z = B ↔ y z z = y ↔ y z z = B
9 equsb1v ⊢ y z z = y
10 9 tbt ⊢ y z z = B ↔ y z z = B ↔ y z z = y
11 bicom ⊢ y z z = B ↔ y z z = y ↔ y z z = y ↔ y z z = B
12 10 11 bitri ⊢ y z z = B ↔ y z z = y ↔ y z z = B
13 eqsb1 ⊢ y z z = B ↔ y = B
14 8 12 13 3bitr2i ⊢ y z z = y ↔ z = B ↔ y = B
15 7 14 sylib ⊢ ∀ z z = y ↔ z = B → y = B
16 6 15 impbii ⊢ y = B ↔ ∀ z z = y ↔ z = B
17 1 4 16 vtoclbg ⊢ A ∈ V → A = B ↔ ∀ z z = A ↔ z = B