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

Theorem elxp5 5361
 Description: Membership in a cross product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 5360 when the double intersection does not create class existence problems (caused by int0 4066). (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 4898 . 2
2 sneq 3827 . . . . . . . . . . . 12
32rneqd 5100 . . . . . . . . . . 11
43unieqd 4028 . . . . . . . . . 10
5 vex 2961 . . . . . . . . . . 11
6 vex 2961 . . . . . . . . . . 11
75, 6op2nda 5357 . . . . . . . . . 10
84, 7syl6req 2487 . . . . . . . . 9
98pm4.71ri 616 . . . . . . . 8
109anbi1i 678 . . . . . . 7
11 anass 632 . . . . . . 7
1210, 11bitri 242 . . . . . 6
1312exbii 1593 . . . . 5
14 snex 4408 . . . . . . . 8
1514rnex 5136 . . . . . . 7
1615uniex 4708 . . . . . 6
17 opeq2 3987 . . . . . . . 8
1817eqeq2d 2449 . . . . . . 7
19 eleq1 2498 . . . . . . . 8
2019anbi2d 686 . . . . . . 7
2118, 20anbi12d 693 . . . . . 6
2216, 21ceqsexv 2993 . . . . 5
2313, 22bitri 242 . . . 4
24 inteq 4055 . . . . . . . 8
2524inteqd 4057 . . . . . . 7
265, 16op1stb 4761 . . . . . . 7
2725, 26syl6req 2487 . . . . . 6
2827pm4.71ri 616 . . . . 5
2928anbi1i 678 . . . 4
30 anass 632 . . . 4
3123, 29, 303bitri 264 . . 3
3231exbii 1593 . 2
33 eleq1 2498 . . . . . 6
345, 33mpbii 204 . . . . 5
3534adantr 453 . . . 4
3635exlimiv 1645 . . 3
37 elex 2966 . . . 4