Theorem unexOLD

Description: Obsolete version of unex as of 21-Jul-2025. (Contributed by NM, 1-Jul-1994) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	unex.1	|- A e. _V
	unex.2	|- B e. _V
Assertion	unexOLD	|- ( A u. B ) e. _V

Proof

Step	Hyp	Ref	Expression
1		unex.1	|- A e. _V
2		unex.2	|- B e. _V
3	1 2	unipr	|- U. { A , B } = ( A u. B )
4		prex	|- { A , B } e. _V
5	4	uniex	|- U. { A , B } e. _V
6	3 5	eqeltrri	|- ( A u. B ) e. _V