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 ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 ∀ 𝑧 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑦 ∈ V
2 csbtt ⊢ ( ( 𝑦 ∈ V ∧ Ⅎ 𝑥 𝐴 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐴 )
3 1 2 mpan ⊢ ( Ⅎ 𝑥 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐴 )
4 vex ⊢ 𝑧 ∈ V
5 csbtt ⊢ ( ( 𝑧 ∈ V ∧ Ⅎ 𝑥 𝐴 ) → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = 𝐴 )
6 4 5 mpan ⊢ ( Ⅎ 𝑥 𝐴 → ⦋ 𝑧 / 𝑥 ⦌ 𝐴 = 𝐴 )
7 3 6 eqtr4d ⊢ ( Ⅎ 𝑥 𝐴 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
8 7 alrimivv ⊢ ( Ⅎ 𝑥 𝐴 → ∀ 𝑦 ∀ 𝑧 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
9 nfv ⊢ Ⅎ 𝑤 ∀ 𝑦 ∀ 𝑧 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴
10 eleq2 ⊢ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → ( 𝑤 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ↔ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 ) )
11 sbsbc ⊢ ( [ 𝑦 / 𝑥 ] 𝑤 ∈ 𝐴 ↔ [ 𝑦 / 𝑥 ] 𝑤 ∈ 𝐴 )
12 sbcel2 ⊢ ( [ 𝑦 / 𝑥 ] 𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
13 11 12 bitri ⊢ ( [ 𝑦 / 𝑥 ] 𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
14 sbsbc ⊢ ( [ 𝑧 / 𝑥 ] 𝑤 ∈ 𝐴 ↔ [ 𝑧 / 𝑥 ] 𝑤 ∈ 𝐴 )
15 sbcel2 ⊢ ( [ 𝑧 / 𝑥 ] 𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
16 14 15 bitri ⊢ ( [ 𝑧 / 𝑥 ] 𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )
17 10 13 16 3bitr4g ⊢ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → ( [ 𝑦 / 𝑥 ] 𝑤 ∈ 𝐴 ↔ [ 𝑧 / 𝑥 ] 𝑤 ∈ 𝐴 ) )
18 17 2alimi ⊢ ( ∀ 𝑦 ∀ 𝑧 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → ∀ 𝑦 ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝑤 ∈ 𝐴 ↔ [ 𝑧 / 𝑥 ] 𝑤 ∈ 𝐴 ) )
19 sbnf2 ⊢ ( Ⅎ 𝑥 𝑤 ∈ 𝐴 ↔ ∀ 𝑦 ∀ 𝑧 ( [ 𝑦 / 𝑥 ] 𝑤 ∈ 𝐴 ↔ [ 𝑧 / 𝑥 ] 𝑤 ∈ 𝐴 ) )
20 18 19 sylibr ⊢ ( ∀ 𝑦 ∀ 𝑧 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → Ⅎ 𝑥 𝑤 ∈ 𝐴 )
21 9 20 nfcd ⊢ ( ∀ 𝑦 ∀ 𝑧 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 → Ⅎ 𝑥 𝐴 )
22 8 21 impbii ⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 ∀ 𝑧 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑧 / 𝑥 ⦌ 𝐴 )