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 X V [˙X / x]˙ F : A B X / x F : X / x A X / x B

Proof

Step Hyp Ref Expression
1 df-f F : A B F Fn A ran F B
2 1 a1i X V F : A B F Fn A ran F B
3 2 sbcbidv X V [˙X / x]˙ F : A B [˙X / x]˙ F Fn A ran F B
4 sbcfng X V [˙X / x]˙ F Fn A X / x F Fn X / x A
5 sbcssg X V [˙X / x]˙ ran F B X / x ran F X / x B
6 csbrn X / x ran F = ran X / x F
7 6 sseq1i X / x ran F X / x B ran X / x F X / x B
8 5 7 bitrdi X V [˙X / x]˙ ran F B ran X / x F X / x B
9 4 8 anbi12d X V [˙X / x]˙ F Fn A [˙X / x]˙ ran F B X / x F Fn X / x A ran X / x F X / x B
10 sbcan [˙X / x]˙ F Fn A ran F B [˙X / x]˙ F Fn A [˙X / x]˙ ran F B
11 df-f X / x F : X / x A X / x B X / x F Fn X / x A ran X / x F X / x B
12 9 10 11 3bitr4g X V [˙X / x]˙ F Fn A ran F B X / x F : X / x A X / x B
13 3 12 bitrd X V [˙X / x]˙ F : A B X / x F : X / x A X / x B