Description: Alternate definition of the conditional operator df-if . Note that ph is independent of x i.e. a constant true or false. (Contributed by NM, 25-Aug-2013) (Revised by Mario Carneiro, 8-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Hypothesis | dfif3.1 | |
|
Assertion | dfif3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfif3.1 | |
|
2 | dfif6 | |
|
3 | biidd | |
|
4 | 3 | cbvabv | |
5 | 1 4 | eqtri | |
6 | 5 | ineq2i | |
7 | dfrab3 | |
|
8 | 6 7 | eqtr4i | |
9 | dfrab3 | |
|
10 | biidd | |
|
11 | 10 | notabw | |
12 | biidd | |
|
13 | 12 | cbvabv | |
14 | 1 13 | eqtri | |
15 | 14 | difeq2i | |
16 | 11 15 | eqtr4i | |
17 | 16 | ineq2i | |
18 | 9 17 | eqtr2i | |
19 | 8 18 | uneq12i | |
20 | 2 19 | eqtr4i | |