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 AV
opeluu.2 BV
Assertion opeluu ABCACBC

Proof

Step Hyp Ref Expression
1 opeluu.1 AV
2 opeluu.2 BV
3 1 prid1 AAB
4 1 2 opi2 ABAB
5 elunii ABABABCABC
6 4 5 mpan ABCABC
7 elunii AABABCAC
8 3 6 7 sylancr ABCAC
9 2 prid2 BAB
10 elunii BABABCBC
11 9 6 10 sylancr ABCBC
12 8 11 jca ABCACBC