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\left(\phi ,A,B\right)=\left\{x|\left(\left(\phi \wedge x\in A\right)\vee \left(\neg \phi \wedge x\in B\right)\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		bj-df-ifc	$$⊢if\left(\phi ,A,B\right)=\left\{x|if-\left(\phi ,x\in A,x\in B\right)\right\}$$
2		df-ifp	$$⊢if-\left(\phi ,x\in A,x\in B\right)\leftrightarrow \left(\left(\phi \wedge x\in A\right)\vee \left(\neg \phi \wedge x\in B\right)\right)$$
3	2	abbii	$$⊢\left\{x|if-\left(\phi ,x\in A,x\in B\right)\right\}=\left\{x|\left(\left(\phi \wedge x\in A\right)\vee \left(\neg \phi \wedge x\in B\right)\right)\right\}$$
4	1 3	eqtri	$$⊢if\left(\phi ,A,B\right)=\left\{x|\left(\left(\phi \wedge x\in A\right)\vee \left(\neg \phi \wedge x\in B\right)\right)\right\}$$