This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. V -> ( A = B <-> A. 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 -> ( A. z ( z = y <-> z = B ) <-> A. z ( z = A <-> z = B ) ) )
5 eqeq2 
 |-  ( y = B -> ( z = y <-> z = B ) )
6 5 alrimiv 
 |-  ( y = B -> A. z ( z = y <-> z = B ) )
7 stdpc4 
 |-  ( A. 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 
 |-  ( A. z ( z = y <-> z = B ) -> y = B )
16 6 15 impbii 
 |-  ( y = B <-> A. z ( z = y <-> z = B ) )
17 1 4 16 vtoclbg 
 |-  ( A e. V -> ( A = B <-> A. z ( z = A <-> z = B ) ) )