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	⊢ 𝐴 ∈ V
	opeluu.2	⊢ 𝐵 ∈ V
Assertion	opeluu	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → ( 𝐴 ∈ ∪ ∪ 𝐶 ∧ 𝐵 ∈ ∪ ∪ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		opeluu.1	⊢ 𝐴 ∈ V
2		opeluu.2	⊢ 𝐵 ∈ V
3	1	prid1	⊢ 𝐴 ∈ { 𝐴 , 𝐵 }
4	1 2	opi2	⊢ { 𝐴 , 𝐵 } ∈ ⟨ 𝐴 , 𝐵 ⟩
5		elunii	⊢ ( ( { 𝐴 , 𝐵 } ∈ ⟨ 𝐴 , 𝐵 ⟩ ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 ) → { 𝐴 , 𝐵 } ∈ ∪ 𝐶 )
6	4 5	mpan	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → { 𝐴 , 𝐵 } ∈ ∪ 𝐶 )
7		elunii	⊢ ( ( 𝐴 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝐵 } ∈ ∪ 𝐶 ) → 𝐴 ∈ ∪ ∪ 𝐶 )
8	3 6 7	sylancr	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → 𝐴 ∈ ∪ ∪ 𝐶 )
9	2	prid2	⊢ 𝐵 ∈ { 𝐴 , 𝐵 }
10		elunii	⊢ ( ( 𝐵 ∈ { 𝐴 , 𝐵 } ∧ { 𝐴 , 𝐵 } ∈ ∪ 𝐶 ) → 𝐵 ∈ ∪ ∪ 𝐶 )
11	9 6 10	sylancr	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → 𝐵 ∈ ∪ ∪ 𝐶 )
12	8 11	jca	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → ( 𝐴 ∈ ∪ ∪ 𝐶 ∧ 𝐵 ∈ ∪ ∪ 𝐶 ) )