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 eqsb3 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