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 ⊢ X ∈ V → [˙X / x]˙ F Fn A ↔ ⦋ X / x⦌ F Fn ⦋ X / x⦌ A

Proof

Step Hyp Ref Expression
1 df-fn ⊢ F Fn A ↔ Fun ⁡ F ∧ dom ⁡ F = A
2 1 a1i ⊢ X ∈ V → F Fn A ↔ Fun ⁡ F ∧ dom ⁡ F = A
3 2 sbcbidv ⊢ X ∈ V → [˙X / x]˙ F Fn A ↔ [˙X / x]˙ Fun ⁡ F ∧ dom ⁡ F = A
4 sbcfung ⊢ X ∈ V → [˙X / x]˙ Fun ⁡ F ↔ Fun ⁡ ⦋ X / x⦌ F
5 sbceqg ⊢ X ∈ V → [˙X / x]˙ dom ⁡ F = A ↔ ⦋ X / x⦌ dom ⁡ F = ⦋ X / x⦌ A
6 csbdm ⊢ ⦋ X / x⦌ dom ⁡ F = dom ⁡ ⦋ X / x⦌ F
7 6 eqeq1i ⊢ ⦋ X / x⦌ dom ⁡ F = ⦋ X / x⦌ A ↔ dom ⁡ ⦋ X / x⦌ F = ⦋ X / x⦌ A
8 5 7 bitrdi ⊢ X ∈ V → [˙X / x]˙ dom ⁡ F = A ↔ dom ⁡ ⦋ X / x⦌ F = ⦋ X / x⦌ A
9 4 8 anbi12d ⊢ X ∈ V → [˙X / x]˙ Fun ⁡ F ∧ [˙X / x]˙ dom ⁡ F = A ↔ Fun ⁡ ⦋ X / x⦌ F ∧ dom ⁡ ⦋ X / x⦌ F = ⦋ X / x⦌ A
10 sbcan ⊢ [˙X / x]˙ Fun ⁡ F ∧ dom ⁡ F = A ↔ [˙X / x]˙ Fun ⁡ F ∧ [˙X / x]˙ dom ⁡ F = A
11 df-fn ⊢ ⦋ X / x⦌ F Fn ⦋ X / x⦌ A ↔ Fun ⁡ ⦋ X / x⦌ F ∧ dom ⁡ ⦋ X / x⦌ F = ⦋ X / x⦌ A
12 9 10 11 3bitr4g ⊢ X ∈ V → [˙X / x]˙ Fun ⁡ F ∧ dom ⁡ F = A ↔ ⦋ X / x⦌ F Fn ⦋ X / x⦌ A
13 3 12 bitrd ⊢ X ∈ V → [˙X / x]˙ F Fn A ↔ ⦋ X / x⦌ F Fn ⦋ X / x⦌ A