Metamath Proof Explorer


Theorem bj-dfif

Description: Alternate definition of the conditional operator for classes, which used to be the main definition. (Contributed by BJ, 26-Dec-2023) (Proof modification is discouraged.)

Ref Expression
Assertion bj-dfif ifφAB=x|φxA¬φxB

Proof

Step Hyp Ref Expression
1 bj-df-ifc ifφAB=x|if-φxAxB
2 df-ifp if-φxAxBφxA¬φxB
3 2 abbii x|if-φxAxB=x|φxA¬φxB
4 1 3 eqtri ifφAB=x|φxA¬φxB