Metamath Proof Explorer

Theorem bnj62

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion bnj62 
|- ( [. z / x ]. x Fn A <-> z Fn A )

Proof

Step Hyp Ref Expression
1 vex 
 |-  y e. _V
2 fneq1 
 |-  ( x = y -> ( x Fn A <-> y Fn A ) )
3 1 2 sbcie 
 |-  ( [. y / x ]. x Fn A <-> y Fn A )
4 3 sbcbii 
 |-  ( [. z / y ]. [. y / x ]. x Fn A <-> [. z / y ]. y Fn A )
5 sbccow 
 |-  ( [. z / y ]. [. y / x ]. x Fn A <-> [. z / x ]. x Fn A )
6 vex 
 |-  z e. _V
7 fneq1 
 |-  ( y = z -> ( y Fn A <-> z Fn A ) )
8 6 7 sbcie 
 |-  ( [. z / y ]. y Fn A <-> z Fn A )
9 4 5 8 3bitr3i 
 |-  ( [. z / x ]. x Fn A <-> z Fn A )