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

Metamath Proof Explorer

Theorem sbnfc2

Description: Two ways of expressing " x is (effectively) not free in A ". (Contributed by Mario Carneiro, 14-Oct-2016)

Ref Expression
Assertion sbnfc2 
|- ( F/_ x A <-> A. y A. z [_ y / x ]_ A = [_ z / x ]_ A )

Proof

Step Hyp Ref Expression
1 vex 
 |-  y e. _V
2 csbtt 
 |-  ( ( y e. _V /\ F/_ x A ) -> [_ y / x ]_ A = A )
3 1 2 mpan 
 |-  ( F/_ x A -> [_ y / x ]_ A = A )
4 vex 
 |-  z e. _V
5 csbtt 
 |-  ( ( z e. _V /\ F/_ x A ) -> [_ z / x ]_ A = A )
6 4 5 mpan 
 |-  ( F/_ x A -> [_ z / x ]_ A = A )
7 3 6 eqtr4d 
 |-  ( F/_ x A -> [_ y / x ]_ A = [_ z / x ]_ A )
8 7 alrimivv 
 |-  ( F/_ x A -> A. y A. z [_ y / x ]_ A = [_ z / x ]_ A )
9 nfv 
 |-  F/ w A. y A. z [_ y / x ]_ A = [_ z / x ]_ A
10 eleq2 
 |-  ( [_ y / x ]_ A = [_ z / x ]_ A -> ( w e. [_ y / x ]_ A <-> w e. [_ z / x ]_ A ) )
11 sbsbc 
 |-  ( [ y / x ] w e. A <-> [. y / x ]. w e. A )
12 sbcel2 
 |-  ( [. y / x ]. w e. A <-> w e. [_ y / x ]_ A )
13 11 12 bitri 
 |-  ( [ y / x ] w e. A <-> w e. [_ y / x ]_ A )
14 sbsbc 
 |-  ( [ z / x ] w e. A <-> [. z / x ]. w e. A )
15 sbcel2 
 |-  ( [. z / x ]. w e. A <-> w e. [_ z / x ]_ A )
16 14 15 bitri 
 |-  ( [ z / x ] w e. A <-> w e. [_ z / x ]_ A )
17 10 13 16 3bitr4g 
 |-  ( [_ y / x ]_ A = [_ z / x ]_ A -> ( [ y / x ] w e. A <-> [ z / x ] w e. A ) )
18 17 2alimi 
 |-  ( A. y A. z [_ y / x ]_ A = [_ z / x ]_ A -> A. y A. z ( [ y / x ] w e. A <-> [ z / x ] w e. A ) )
19 sbnf2 
 |-  ( F/ x w e. A <-> A. y A. z ( [ y / x ] w e. A <-> [ z / x ] w e. A ) )
20 18 19 sylibr 
 |-  ( A. y A. z [_ y / x ]_ A = [_ z / x ]_ A -> F/ x w e. A )
21 9 20 nfcd 
 |-  ( A. y A. z [_ y / x ]_ A = [_ z / x ]_ A -> F/_ x A )
22 8 21 impbii 
 |-  ( F/_ x A <-> A. y A. z [_ y / x ]_ A = [_ z / x ]_ A )