Step | Hyp | Ref
| Expression |
1 | | ssel 3267 |
. . 3
![(](lp.gif) 1c ![(](lp.gif)
1c![)](rp.gif) ![)](rp.gif) |
2 | | pw1ss1c 4158 |
. . . . 5
1 ![U.](bigcup.gif) 1c |
3 | 2 | sseli 3269 |
. . . 4
![(](lp.gif) 1 ![U.](bigcup.gif) 1c![)](rp.gif) |
4 | 3 | a1i 10 |
. . 3
![(](lp.gif) 1c ![(](lp.gif) 1 ![U.](bigcup.gif) 1c![)](rp.gif) ![)](rp.gif) |
5 | | el1c 4139 |
. . . 4
![(](lp.gif) 1c ![E.](exists.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) |
6 | | vex 2862 |
. . . . . . . . . 10
![_V](rmcv.gif) |
7 | 6 | snid 3760 |
. . . . . . . . 9
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) |
8 | | eleq2 2414 |
. . . . . . . . . 10
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 8 | rspcev 2955 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![{](lbrace.gif) ![y](_y.gif) ![}](rbrace.gif) ![E.](exists.gif)
![x](_x.gif) ![)](rp.gif) |
10 | 7, 9 | mpan2 652 |
. . . . . . . 8
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![E.](exists.gif) ![x](_x.gif) ![)](rp.gif) |
11 | | el1c 4139 |
. . . . . . . . . . 11
![(](lp.gif) 1c ![E.](exists.gif)
![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![)](rp.gif) |
12 | | elsn 3748 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif)
![z](_z.gif) ![)](rp.gif) |
13 | | sneq 3744 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![)](rp.gif) |
14 | 13 | eleq1d 2419 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![{](lbrace.gif) ![z](_z.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 12, 14 | sylbi 187 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![{](lbrace.gif) ![z](_z.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 15 | biimprcd 216 |
. . . . . . . . . . . . 13
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![(](lp.gif)
![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![y](_y.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
17 | | eleq1 2413 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | eleq2 2414 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![(](lp.gif)
![{](lbrace.gif) ![z](_z.gif) ![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
19 | 18 | imbi1d 308 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif)
![A](_ca.gif) ![(](lp.gif)
![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![y](_y.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
20 | 17, 19 | imbi12d 311 |
. . . . . . . . . . . . 13
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![A](_ca.gif) ![)](rp.gif) ![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif)
![(](lp.gif)
![{](lbrace.gif) ![z](_z.gif) ![{](lbrace.gif) ![y](_y.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 16, 20 | mpbiri 224 |
. . . . . . . . . . . 12
![(](lp.gif) ![{](lbrace.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 21 | exlimiv 1634 |
. . . . . . . . . . 11
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
![{](lbrace.gif) ![y](_y.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 11, 22 | sylbi 187 |
. . . . . . . . . 10
![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | 1, 23 | syli 33 |
. . . . . . . . 9
![(](lp.gif) 1c ![(](lp.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
25 | 24 | rexlimdv 2737 |
. . . . . . . 8
![(](lp.gif) 1c ![(](lp.gif) ![E.](exists.gif) ![{](lbrace.gif) ![y](_y.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 10, 25 | impbid2 195 |
. . . . . . 7
![(](lp.gif) 1c ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![E.](exists.gif) ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
27 | | eluni2 3895 |
. . . . . . 7
![(](lp.gif) ![U.](bigcup.gif) ![E.](exists.gif) ![x](_x.gif) ![)](rp.gif) |
28 | 26, 27 | syl6bbr 254 |
. . . . . 6
![(](lp.gif) 1c ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![U.](bigcup.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
29 | | eleq1 2413 |
. . . . . . 7
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
30 | | eleq1 2413 |
. . . . . . . 8
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) 1 ![U.](bigcup.gif) ![{](lbrace.gif) ![y](_y.gif) 1 ![U.](bigcup.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
31 | | snelpw1 4146 |
. . . . . . . 8
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) 1 ![U.](bigcup.gif)
![U.](bigcup.gif) ![A](_ca.gif) ![)](rp.gif) |
32 | 30, 31 | syl6bb 252 |
. . . . . . 7
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) 1 ![U.](bigcup.gif) ![U.](bigcup.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 29, 32 | bibi12d 312 |
. . . . . 6
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) ![(](lp.gif) 1 ![U.](bigcup.gif) ![A](_ca.gif)
![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![U.](bigcup.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | 28, 33 | syl5ibrcom 213 |
. . . . 5
![(](lp.gif) 1c ![(](lp.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif) 1 ![U.](bigcup.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
35 | 34 | exlimdv 1636 |
. . . 4
![(](lp.gif) 1c ![(](lp.gif) ![E.](exists.gif) ![{](lbrace.gif) ![y](_y.gif) ![(](lp.gif)
1 ![U.](bigcup.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 5, 35 | syl5bi 208 |
. . 3
![(](lp.gif) 1c ![(](lp.gif) 1c ![(](lp.gif)
1 ![U.](bigcup.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 1, 4, 36 | pm5.21ndd 343 |
. 2
![(](lp.gif) 1c ![(](lp.gif)
1 ![U.](bigcup.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 37 | eqrdv 2351 |
1
![(](lp.gif) 1c 1 ![U.](bigcup.gif) ![A](_ca.gif) ![)](rp.gif) |