This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (φ, A, B) \subseteq A \cup B$

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