Theorem bj-df-ifc

Description: Candidate definition for the conditional operator for classes. This is in line with the definition of a class as the extension of a predicate in df-clab . We reprove the current df-if from it in bj-dfif . (Contributed by BJ, 20-Sep-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-df-ifc	$$⊢if\left(\phi ,A,B\right)=\left\{x|if-\left(\phi ,x\in A,x\in B\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-if	$$⊢if\left(\phi ,A,B\right)=\left\{x|\left(\left(x\in A\wedge \phi \right)\vee \left(x\in B\wedge \neg \phi \right)\right)\right\}$$
2		ancom	$$⊢\left(x\in A\wedge \phi \right)\leftrightarrow \left(\phi \wedge x\in A\right)$$
3		ancom	$$⊢\left(x\in B\wedge \neg \phi \right)\leftrightarrow \left(\neg \phi \wedge x\in B\right)$$
4	2 3	orbi12i	$$⊢\left(\left(x\in A\wedge \phi \right)\vee \left(x\in B\wedge \neg \phi \right)\right)\leftrightarrow \left(\left(\phi \wedge x\in A\right)\vee \left(\neg \phi \wedge x\in B\right)\right)$$
5		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)$$
6	4 5	bitr4i	$$⊢\left(\left(x\in A\wedge \phi \right)\vee \left(x\in B\wedge \neg \phi \right)\right)\leftrightarrow if-\left(\phi ,x\in A,x\in B\right)$$
7	6	abbii	$$⊢\left\{x|\left(\left(x\in A\wedge \phi \right)\vee \left(x\in B\wedge \neg \phi \right)\right)\right\}=\left\{x|if-\left(\phi ,x\in A,x\in B\right)\right\}$$
8	1 7	eqtri	$$⊢if\left(\phi ,A,B\right)=\left\{x|if-\left(\phi ,x\in A,x\in B\right)\right\}$$