Theorem uniopel

Description: Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypotheses	opthw.1	|- A e. _V
	opthw.2	|- B e. _V
Assertion	uniopel	|- ( <. A , B >. e. C -> U. <. A , B >. e. U. C )

Proof

Step	Hyp	Ref	Expression
1		opthw.1	|- A e. _V
2		opthw.2	|- B e. _V
3	1 2	uniop	|- U. <. A , B >. = { A , B }
4	1 2	opi2	|- { A , B } e. <. A , B >.
5	3 4	eqeltri	|- U. <. A , B >. e. <. A , B >.
6		elssuni	|- ( <. A , B >. e. C -> <. A , B >. C_ U. C )
7	6	sseld	|- ( <. A , B >. e. C -> ( U. <. A , B >. e. <. A , B >. -> U. <. A , B >. e. U. C ) )
8	5 7	mpi	|- ( <. A , B >. e. C -> U. <. A , B >. e. U. C )