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 e. 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 e. V -> ( F Fn A <-> ( Fun F /\ dom F = A ) ) )
3	2	sbcbidv	|- ( X e. V -> ( [. X / x ]. F Fn A <-> [. X / x ]. ( Fun F /\ dom F = A ) ) )
4		sbcfung	|- ( X e. V -> ( [. X / x ]. Fun F <-> Fun [_ X / x ]_ F ) )
5		sbceqg	|- ( X e. 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 e. V -> ( [. X / x ]. dom F = A <-> dom [_ X / x ]_ F = [_ X / x ]_ A ) )
9	4 8	anbi12d	|- ( X e. 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 e. V -> ( [. X / x ]. ( Fun F /\ dom F = A ) <-> [_ X / x ]_ F Fn [_ X / x ]_ A ) )
13	3 12	bitrd	|- ( X e. V -> ( [. X / x ]. F Fn A <-> [_ X / x ]_ F Fn [_ X / x ]_ A ) )