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 ( ph , A , B ) C_ ( A u. B )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- { x | ph } = { x | ph }
2	1	dfif4	|- if ( ph , A , B ) = ( ( A u. B ) i^i ( ( A u. ( _V \ { x | ph } ) ) i^i ( B u. { x | ph } ) ) )
3		inss1	|- ( ( A u. B ) i^i ( ( A u. ( _V \ { x | ph } ) ) i^i ( B u. { x | ph } ) ) ) C_ ( A u. B )
4	2 3	eqsstri	|- if ( ph , A , B ) C_ ( A u. B )