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 eqsb1 ⊢ y z z = B ↔ y = B
10 9 bibi2i ⊢ y z z = y ↔ y z z = B ↔ y z z = y ↔ y = B
11 equsb1v ⊢ y z z = y
12 biimp ⊢ y z z = y ↔ y = B → y z z = y → y = B
13 11 12 mpi ⊢ y z z = y ↔ y = B → y = B
14 10 13 sylbi ⊢ y z z = y ↔ y z z = B → y = B
15 8 14 sylbi ⊢ y z z = y ↔ z = B → y = B
16 7 15 syl ⊢ ∀ z z = y ↔ z = B → y = B
17 6 16 impbii ⊢ y = B ↔ ∀ z z = y ↔ z = B
18 1 4 17 vtoclbg ⊢ A ∈ V → A = B ↔ ∀ z z = A ↔ z = B