Theorem bj-ififc

Description: A biconditional connecting the conditional operator for propositions and the conditional operator for classes. Note that there is no sethood hypothesis on X : it is implied by either side. (Contributed by BJ, 24-Sep-2019) Generalize statement from setvar x to class X . (Revised by BJ, 26-Dec-2023)

	Ref	Expression
Assertion	bj-ififc	$$⊢X\in if\left(\phi ,A,B\right)\leftrightarrow if-\left(\phi ,X\in A,X\in B\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	1	eleq2i	$$⊢X\in if\left(\phi ,A,B\right)\leftrightarrow X\in \left\{x|if-\left(\phi ,x\in A,x\in B\right)\right\}$$
3		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)$$
4		elex	$$⊢X\in A\to X\in \mathrm{V}$$
5	4	adantl	$$⊢\left(\phi \wedge X\in A\right)\to X\in \mathrm{V}$$
6		elex	$$⊢X\in B\to X\in \mathrm{V}$$
7	6	adantl	$$⊢\left(\neg \phi \wedge X\in B\right)\to X\in \mathrm{V}$$
8	5 7	jaoi	$$⊢\left(\left(\phi \wedge X\in A\right)\vee \left(\neg \phi \wedge X\in B\right)\right)\to X\in \mathrm{V}$$
9	3 8	sylbi	$$⊢if-\left(\phi ,X\in A,X\in B\right)\to X\in \mathrm{V}$$
10		eleq1	$$⊢x=X\to \left(x\in A\leftrightarrow X\in A\right)$$
11		eleq1	$$⊢x=X\to \left(x\in B\leftrightarrow X\in B\right)$$
12	10 11	ifpbi23d	$$⊢x=X\to \left(if-\left(\phi ,x\in A,x\in B\right)\leftrightarrow if-\left(\phi ,X\in A,X\in B\right)\right)$$
13	9 12	elab3	$$⊢X\in \left\{x|if-\left(\phi ,x\in A,x\in B\right)\right\}\leftrightarrow if-\left(\phi ,X\in A,X\in B\right)$$
14	2 13	bitri	$$⊢X\in if\left(\phi ,A,B\right)\leftrightarrow if-\left(\phi ,X\in A,X\in B\right)$$