iotassuni

Description: The iota class is a subset of the union of all elements satisfying ph . (Contributed by Mario Carneiro, 24-Dec-2016) Remove dependency on ax-10 , ax-11 , ax-12 . (Revised by SN, 6-Nov-2024)

		Ref	Expression
	Assertion	iotassuni	$⊢ (ι x \| φ) \subseteq ⋃ \{x \| φ\}$

Proof

Step	Hyp	Ref	Expression
1		iotauni2	$⊢ \exists y \{x \| φ\} = \{y\} \to (ι x \| φ) = ⋃ \{x \| φ\}$
2		eqimss	$⊢ (ι x \| φ) = ⋃ \{x \| φ\} \to (ι x \| φ) \subseteq ⋃ \{x \| φ\}$
3	1 2	syl	$⊢ \exists y \{x \| φ\} = \{y\} \to (ι x \| φ) \subseteq ⋃ \{x \| φ\}$
4		iotanul2	$⊢ \neg \exists y \{x \| φ\} = \{y\} \to (ι x \| φ) = \emptyset$
5		0ss	$⊢ \emptyset \subseteq ⋃ \{x \| φ\}$
6	4 5	eqsstrdi	$⊢ \neg \exists y \{x \| φ\} = \{y\} \to (ι x \| φ) \subseteq ⋃ \{x \| φ\}$
7	3 6	pm2.61i	$⊢ (ι x \| φ) \subseteq ⋃ \{x \| φ\}$

Metamath Proof Explorer

Theorem iotassuni

Proof