Theorem opeluu

Description: Each member of an ordered pair belongs to the union of the union of a class to which the ordered pair belongs. Lemma 3D of Enderton p. 41. (Contributed by NM, 31-Mar-1995) (Revised by Mario Carneiro, 27-Feb-2016)

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

Proof

Step	Hyp	Ref	Expression
1		opeluu.1	|- A e. _V
2		opeluu.2	|- B e. _V
3	1	prid1	|- A e. { A , B }
4	1 2	opi2	|- { A , B } e. <. A , B >.
5		elunii	|- ( ( { A , B } e. <. A , B >. /\ <. A , B >. e. C ) -> { A , B } e. U. C )
6	4 5	mpan	|- ( <. A , B >. e. C -> { A , B } e. U. C )
7		elunii	|- ( ( A e. { A , B } /\ { A , B } e. U. C ) -> A e. U. U. C )
8	3 6 7	sylancr	|- ( <. A , B >. e. C -> A e. U. U. C )
9	2	prid2	|- B e. { A , B }
10		elunii	|- ( ( B e. { A , B } /\ { A , B } e. U. C ) -> B e. U. U. C )
11	9 6 10	sylancr	|- ( <. A , B >. e. C -> B e. U. U. C )
12	8 11	jca	|- ( <. A , B >. e. C -> ( A e. U. U. C /\ B e. U. U. C ) )