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 XV[˙X/x]˙FFnAX/xFFnX/xA

Proof

Step Hyp Ref Expression
1 df-fn FFnAFunFdomF=A
2 1 a1i XVFFnAFunFdomF=A
3 2 sbcbidv XV[˙X/x]˙FFnA[˙X/x]˙FunFdomF=A
4 sbcfung XV[˙X/x]˙FunFFunX/xF
5 sbceqg XV[˙X/x]˙domF=AX/xdomF=X/xA
6 csbdm X/xdomF=domX/xF
7 6 eqeq1i X/xdomF=X/xAdomX/xF=X/xA
8 5 7 bitrdi XV[˙X/x]˙domF=AdomX/xF=X/xA
9 4 8 anbi12d XV[˙X/x]˙FunF[˙X/x]˙domF=AFunX/xFdomX/xF=X/xA
10 sbcan [˙X/x]˙FunFdomF=A[˙X/x]˙FunF[˙X/x]˙domF=A
11 df-fn X/xFFnX/xAFunX/xFdomX/xF=X/xA
12 9 10 11 3bitr4g XV[˙X/x]˙FunFdomF=AX/xFFnX/xA
13 3 12 bitrd XV[˙X/x]˙FFnAX/xFFnX/xA