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

Metamath Proof Explorer

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 ⊢ ( 𝑋 ∈ 𝑉 → ( [ 𝑋 / 𝑥 ] 𝐹 : 𝐴 ⟶ 𝐵 ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐹 : ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ⟶ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )