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 ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )