Description: An alternate definition of the conditional operator df-if as a simple class abstraction. (Contributed by Mario Carneiro, 8-Sep-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | dfif6 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unab | ||
2 | df-rab | ||
3 | df-rab | ||
4 | 2 3 | uneq12i | |
5 | df-if | ||
6 | 1 4 5 | 3eqtr4ri |