Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  elxp5 Structured version   Unicode version

Theorem elxp5 6696
 Description: Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 6695 when the double intersection does not create class existence problems (caused by int0 4212). (Contributed by NM, 1-Aug-2004.)
Assertion
Ref Expression
elxp5

Proof of Theorem elxp5
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp 4813 . 2
2 sneq 3951 . . . . . . . . . . . 12
32rneqd 5024 . . . . . . . . . . 11
43unieqd 4172 . . . . . . . . . 10
5 vex 3025 . . . . . . . . . . 11
6 vex 3025 . . . . . . . . . . 11
75, 6op2nda 5283 . . . . . . . . . 10
84, 7syl6req 2479 . . . . . . . . 9
98pm4.71ri 637 . . . . . . . 8
109anbi1i 699 . . . . . . 7
11 anass 653 . . . . . . 7
1210, 11bitri 252 . . . . . 6
1312exbii 1712 . . . . 5
14 snex 4605 . . . . . . . 8
1514rnex 6685 . . . . . . 7
1615uniex 6545 . . . . . 6
17 opeq2 4131 . . . . . . . 8
1817eqeq2d 2438 . . . . . . 7
19 eleq1 2494 . . . . . . . 8
2019anbi2d 708 . . . . . . 7
2118, 20anbi12d 715 . . . . . 6
2216, 21ceqsexv 3060 . . . . 5
2313, 22bitri 252 . . . 4
24 inteq 4201 . . . . . . . 8
2524inteqd 4203 . . . . . . 7
265, 16op1stb 4634 . . . . . . 7
2725, 26syl6req 2479 . . . . . 6
2827pm4.71ri 637 . . . . 5
2928anbi1i 699 . . . 4
30 anass 653 . . . 4
3123, 29, 303bitri 274 . . 3
3231exbii 1712 . 2
33 eqvisset 3030 . . . . 5
3433adantr 466 . . . 4
3534exlimiv 1770 . . 3
36 elex 3031 . . . 4