Theorem uni0OLD

Description: Obsolete version of uni0 as of 1-Feb-2026. (Contributed by NM, 16-Sep-1993) Remove use of ax-nul . (Revised by Eric Schmidt, 4-Apr-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	uni0OLD	$$⊢\bigcup \varnothing =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq \left\{\varnothing \right\}$$
2		uni0b	$$⊢\bigcup \varnothing =\varnothing \leftrightarrow \varnothing \subseteq \left\{\varnothing \right\}$$
3	1 2	mpbir	$$⊢\bigcup \varnothing =\varnothing$$