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

Metamath Proof Explorer

Theorem sbcfng

Description: Distribute proper substitution through the function predicate with a domain. (Contributed by Alexander van der Vekens, 15-Jul-2018)

Ref Expression
Assertion sbcfng ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] 𝐹 Fn 𝐴 ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐹 Fn ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 df-fn ⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) )
2 1 a1i ⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) ) )
3 2 sbcbidv ⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] 𝐹 Fn 𝐴 ↔ [ 𝑋 / 𝑥 ] ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) ) )
4 sbcfung ⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] Fun 𝐹 ↔ Fun ⦋ 𝑋 / 𝑥 ⦌ 𝐹 ) )
5 sbceqg ⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] dom 𝐹 = 𝐴 ↔ ⦋ 𝑋 / 𝑥 ⦌ dom 𝐹 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
6 csbdm ⊢ ⦋ 𝑋 / 𝑥 ⦌ dom 𝐹 = dom ⦋ 𝑋 / 𝑥 ⦌ 𝐹
7 6 eqeq1i ⊢ ( ⦋ 𝑋 / 𝑥 ⦌ dom 𝐹 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ↔ dom ⦋ 𝑋 / 𝑥 ⦌ 𝐹 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 )
8 5 7 bitrdi ⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] dom 𝐹 = 𝐴 ↔ dom ⦋ 𝑋 / 𝑥 ⦌ 𝐹 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
9 4 8 anbi12d ⊢ ( 𝑋 ∈ 𝑉 → ( ( [ 𝑋 / 𝑥 ] Fun 𝐹 ∧ [ 𝑋 / 𝑥 ] dom 𝐹 = 𝐴 ) ↔ ( Fun ⦋ 𝑋 / 𝑥 ⦌ 𝐹 ∧ dom ⦋ 𝑋 / 𝑥 ⦌ 𝐹 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
10 sbcan ⊢ ( [ 𝑋 / 𝑥 ] ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) ↔ ( [ 𝑋 / 𝑥 ] Fun 𝐹 ∧ [ 𝑋 / 𝑥 ] dom 𝐹 = 𝐴 ) )
11 df-fn ⊢ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐹 Fn ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ↔ ( Fun ⦋ 𝑋 / 𝑥 ⦌ 𝐹 ∧ dom ⦋ 𝑋 / 𝑥 ⦌ 𝐹 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
12 9 10 11 3bitr4g ⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐹 Fn ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
13 3 12 bitrd ⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] 𝐹 Fn 𝐴 ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐹 Fn ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )