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\in V\to \left(A=B\leftrightarrow \forall z\left(z=A\leftrightarrow z=B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		eqeq1	$$⊢y=A\to \left(y=B\leftrightarrow A=B\right)$$
2		eqeq2	$$⊢y=A\to \left(z=y\leftrightarrow z=A\right)$$
3	2	bibi1d	$$⊢y=A\to \left(\left(z=y\leftrightarrow z=B\right)\leftrightarrow \left(z=A\leftrightarrow z=B\right)\right)$$
4	3	albidv	$$⊢y=A\to \left(\forall z\left(z=y\leftrightarrow z=B\right)\leftrightarrow \forall z\left(z=A\leftrightarrow z=B\right)\right)$$
5		eqeq2	$$⊢y=B\to \left(z=y\leftrightarrow z=B\right)$$
6	5	alrimiv	$$⊢y=B\to \forall z\left(z=y\leftrightarrow z=B\right)$$
7		stdpc4	$$⊢\forall z\left(z=y\leftrightarrow z=B\right)\to \left[y/z\right]\left(z=y\leftrightarrow z=B\right)$$
8		sbbi	$$⊢\left[y/z\right]\left(z=y\leftrightarrow z=B\right)\leftrightarrow \left(\left[y/z\right]z=y\leftrightarrow \left[y/z\right]z=B\right)$$
9		eqsb1	$$⊢\left[y/z\right]z=B\leftrightarrow y=B$$
10	9	bibi2i	$$⊢\left(\left[y/z\right]z=y\leftrightarrow \left[y/z\right]z=B\right)\leftrightarrow \left(\left[y/z\right]z=y\leftrightarrow y=B\right)$$
11		equsb1v	$$⊢\left[y/z\right]z=y$$
12		biimp	$$⊢\left(\left[y/z\right]z=y\leftrightarrow y=B\right)\to \left(\left[y/z\right]z=y\to y=B\right)$$
13	11 12	mpi	$$⊢\left(\left[y/z\right]z=y\leftrightarrow y=B\right)\to y=B$$
14	10 13	sylbi	$$⊢\left(\left[y/z\right]z=y\leftrightarrow \left[y/z\right]z=B\right)\to y=B$$
15	8 14	sylbi	$$⊢\left[y/z\right]\left(z=y\leftrightarrow z=B\right)\to y=B$$
16	7 15	syl	$$⊢\forall z\left(z=y\leftrightarrow z=B\right)\to y=B$$
17	6 16	impbii	$$⊢y=B\leftrightarrow \forall z\left(z=y\leftrightarrow z=B\right)$$
18	1 4 17	vtoclbg	$$⊢A\in V\to \left(A=B\leftrightarrow \forall z\left(z=A\leftrightarrow z=B\right)\right)$$