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 ( 𝜑 , 𝐴 , 𝐵 ) ⊆ ( 𝐴 ∪ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜑 }
2	1	dfif4	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = ( ( 𝐴 ∪ 𝐵 ) ∩ ( ( 𝐴 ∪ ( V ∖ { 𝑥 ∣ 𝜑 } ) ) ∩ ( 𝐵 ∪ { 𝑥 ∣ 𝜑 } ) ) )
3		inss1	⊢ ( ( 𝐴 ∪ 𝐵 ) ∩ ( ( 𝐴 ∪ ( V ∖ { 𝑥 ∣ 𝜑 } ) ) ∩ ( 𝐵 ∪ { 𝑥 ∣ 𝜑 } ) ) ) ⊆ ( 𝐴 ∪ 𝐵 )
4	2 3	eqsstri	⊢ if ( 𝜑 , 𝐴 , 𝐵 ) ⊆ ( 𝐴 ∪ 𝐵 )