Description: Distribute proper substitution through the function predicate with a domain. (Contributed by Alexander van der Vekens, 15-Jul-2018)
Ref | Expression | ||
---|---|---|---|
Assertion | sbcfng | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fn | |
|
2 | 1 | a1i | |
3 | 2 | sbcbidv | |
4 | sbcfung | |
|
5 | sbceqg | |
|
6 | csbdm | |
|
7 | 6 | eqeq1i | |
8 | 5 7 | bitrdi | |
9 | 4 8 | anbi12d | |
10 | sbcan | |
|
11 | df-fn | |
|
12 | 9 10 11 | 3bitr4g | |
13 | 3 12 | bitrd | |