Theorem ifssun

Description: A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024)

	Ref	Expression
Assertion	ifssun	$$⊢if\left(\phi ,A,B\right)\subseteq A\cup B$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left\{x|\phi \right\}=\left\{x|\phi \right\}$$
2	1	dfif4	$$⊢if\left(\phi ,A,B\right)=\left(A\cup B\right)\cap \left(\left(A\cup \left(\mathrm{V}\setminus \left\{x|\phi \right\}\right)\right)\cap \left(B\cup \left\{x|\phi \right\}\right)\right)$$
3		inss1	$$⊢\left(A\cup B\right)\cap \left(\left(A\cup \left(\mathrm{V}\setminus \left\{x|\phi \right\}\right)\right)\cap \left(B\cup \left\{x|\phi \right\}\right)\right)\subseteq A\cup B$$
4	2 3	eqsstri	$$⊢if\left(\phi ,A,B\right)\subseteq A\cup B$$