# 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}\in {V}\to \left({A}={B}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={A}↔{z}={B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 eqeq1 ${⊢}{y}={A}\to \left({y}={B}↔{A}={B}\right)$
2 eqeq2 ${⊢}{y}={A}\to \left({z}={y}↔{z}={A}\right)$
3 2 bibi1d ${⊢}{y}={A}\to \left(\left({z}={y}↔{z}={B}\right)↔\left({z}={A}↔{z}={B}\right)\right)$
4 3 albidv ${⊢}{y}={A}\to \left(\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}↔{z}={B}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={A}↔{z}={B}\right)\right)$
5 eqeq2 ${⊢}{y}={B}\to \left({z}={y}↔{z}={B}\right)$
6 5 alrimiv ${⊢}{y}={B}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}↔{z}={B}\right)$
7 stdpc4 ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}↔{z}={B}\right)\to \left[{y}/{z}\right]\left({z}={y}↔{z}={B}\right)$
8 sbbi ${⊢}\left[{y}/{z}\right]\left({z}={y}↔{z}={B}\right)↔\left(\left[{y}/{z}\right]{z}={y}↔\left[{y}/{z}\right]{z}={B}\right)$
9 eqsb3 ${⊢}\left[{y}/{z}\right]{z}={B}↔{y}={B}$
10 9 bibi2i ${⊢}\left(\left[{y}/{z}\right]{z}={y}↔\left[{y}/{z}\right]{z}={B}\right)↔\left(\left[{y}/{z}\right]{z}={y}↔{y}={B}\right)$
11 equsb1v ${⊢}\left[{y}/{z}\right]{z}={y}$
12 biimp ${⊢}\left(\left[{y}/{z}\right]{z}={y}↔{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}↔{y}={B}\right)\to {y}={B}$
14 10 13 sylbi ${⊢}\left(\left[{y}/{z}\right]{z}={y}↔\left[{y}/{z}\right]{z}={B}\right)\to {y}={B}$
15 8 14 sylbi ${⊢}\left[{y}/{z}\right]\left({z}={y}↔{z}={B}\right)\to {y}={B}$
16 7 15 syl ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}↔{z}={B}\right)\to {y}={B}$
17 6 16 impbii ${⊢}{y}={B}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={y}↔{z}={B}\right)$
18 1 4 17 vtoclbg ${⊢}{A}\in {V}\to \left({A}={B}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left({z}={A}↔{z}={B}\right)\right)$