Metamath Proof Explorer

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 ∈ V
opeluu.2 ⊢ B ∈ V
Assertion opeluu ⊢ A B ∈ C → A ∈ ⋃ ⋃ C ∧ B ∈ ⋃ ⋃ C

Proof

Step Hyp Ref Expression
1 opeluu.1 ⊢ A ∈ V
2 opeluu.2 ⊢ B ∈ V
3 1 prid1 ⊢ A ∈ A B
4 1 2 opi2 ⊢ A B ∈ A B
5 elunii ⊢ A B ∈ A B ∧ A B ∈ C → A B ∈ ⋃ C
6 4 5 mpan ⊢ A B ∈ C → A B ∈ ⋃ C
7 elunii ⊢ A ∈ A B ∧ A B ∈ ⋃ C → A ∈ ⋃ ⋃ C
8 3 6 7 sylancr ⊢ A B ∈ C → A ∈ ⋃ ⋃ C
9 2 prid2 ⊢ B ∈ A B
10 elunii ⊢ B ∈ A B ∧ A B ∈ ⋃ C → B ∈ ⋃ ⋃ C
11 9 6 10 sylancr ⊢ A B ∈ C → B ∈ ⋃ ⋃ C
12 8 11 jca ⊢ A B ∈ C → A ∈ ⋃ ⋃ C ∧ B ∈ ⋃ ⋃ C