Theorem sbcfg

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

	Ref	Expression
Assertion	sbcfg	⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] 𝐹 : 𝐴 ⟶ 𝐵 ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐹 : ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ⟶ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-f	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
2	1	a1i	⊢ ( 𝑋 ∈ 𝑉 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ) )
3	2	sbcbidv	⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] 𝐹 : 𝐴 ⟶ 𝐵 ↔ [ 𝑋 / 𝑥 ] ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ) )
4		sbcfng	⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] 𝐹 Fn 𝐴 ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐹 Fn ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
5		sbcssg	⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] ran 𝐹 ⊆ 𝐵 ↔ ⦋ 𝑋 / 𝑥 ⦌ ran 𝐹 ⊆ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
6		csbrn	⊢ ⦋ 𝑋 / 𝑥 ⦌ ran 𝐹 = ran ⦋ 𝑋 / 𝑥 ⦌ 𝐹
7	6	sseq1i	⊢ ( ⦋ 𝑋 / 𝑥 ⦌ ran 𝐹 ⊆ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ↔ ran ⦋ 𝑋 / 𝑥 ⦌ 𝐹 ⊆ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
8	5 7	bitrdi	⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] ran 𝐹 ⊆ 𝐵 ↔ ran ⦋ 𝑋 / 𝑥 ⦌ 𝐹 ⊆ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
9	4 8	anbi12d	⊢ ( 𝑋 ∈ 𝑉 → ( ( [ 𝑋 / 𝑥 ] 𝐹 Fn 𝐴 ∧ [ 𝑋 / 𝑥 ] ran 𝐹 ⊆ 𝐵 ) ↔ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐹 Fn ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∧ ran ⦋ 𝑋 / 𝑥 ⦌ 𝐹 ⊆ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) )
10		sbcan	⊢ ( [ 𝑋 / 𝑥 ] ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ↔ ( [ 𝑋 / 𝑥 ] 𝐹 Fn 𝐴 ∧ [ 𝑋 / 𝑥 ] ran 𝐹 ⊆ 𝐵 ) )
11		df-f	⊢ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐹 : ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ⟶ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ↔ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐹 Fn ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∧ ran ⦋ 𝑋 / 𝑥 ⦌ 𝐹 ⊆ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
12	9 10 11	3bitr4g	⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐹 : ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ⟶ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
13	3 12	bitrd	⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] 𝐹 : 𝐴 ⟶ 𝐵 ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐹 : ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ⟶ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )