Step | Hyp | Ref
| Expression |
1 | | df-op 4566 |
. 2
Proj1 ![A](_ca.gif) Proj2 ![A](_ca.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif)
Proj1 ![A](_ca.gif)
Phi ![y](_y.gif) ![{](lbrace.gif)
![E.](exists.gif) Proj2 ![A](_ca.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
2 | | df-proj1 4567 |
. . . . . . 7
Proj1 ![{](lbrace.gif) Phi ![A](_ca.gif) ![}](rbrace.gif) |
3 | 2 | rexeqi 2812 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif)
Proj1 ![A](_ca.gif)
Phi ![E.](exists.gif) ![{](lbrace.gif)
Phi ![A](_ca.gif) ![}](rbrace.gif)
Phi ![y](_y.gif) ![)](rp.gif) |
4 | | phieq 4570 |
. . . . . . . 8
![(](lp.gif)
Phi Phi
![y](_y.gif) ![)](rp.gif) |
5 | 4 | eleq1d 2419 |
. . . . . . 7
![(](lp.gif) Phi Phi ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
6 | 5 | rexab 2999 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) Phi ![A](_ca.gif) ![}](rbrace.gif) Phi ![E.](exists.gif) ![y](_y.gif) Phi Phi ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
7 | | ancom 437 |
. . . . . . . . 9
![(](lp.gif) Phi Phi ![y](_y.gif) ![(](lp.gif) Phi
Phi ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
8 | | eleq1 2413 |
. . . . . . . . . 10
![(](lp.gif) Phi ![(](lp.gif) Phi ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
9 | 8 | pm5.32i 618 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Phi ![A](_ca.gif) ![(](lp.gif) Phi Phi ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
10 | 7, 9 | bitr4i 243 |
. . . . . . . 8
![(](lp.gif) Phi Phi ![y](_y.gif) ![(](lp.gif) Phi
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 10 | exbii 1582 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) Phi
Phi ![y](_y.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
Phi ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
12 | | 19.41v 1901 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Phi
![A](_ca.gif) ![(](lp.gif) ![E.](exists.gif)
Phi ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | ancom 437 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Phi
![A](_ca.gif) ![(](lp.gif)
![E.](exists.gif) Phi ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
14 | 11, 12, 13 | 3bitri 262 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) Phi
Phi ![y](_y.gif) ![(](lp.gif) ![E.](exists.gif)
Phi ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
15 | 3, 6, 14 | 3bitri 262 |
. . . . 5
![(](lp.gif) ![E.](exists.gif)
Proj1 ![A](_ca.gif)
Phi ![(](lp.gif) ![E.](exists.gif)
Phi ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
16 | 15 | abbii 2465 |
. . . 4
![{](lbrace.gif) ![E.](exists.gif)
Proj1 ![A](_ca.gif) Phi ![y](_y.gif) ![{](lbrace.gif) ![(](lp.gif) ![E.](exists.gif) Phi
![y](_y.gif) ![)](rp.gif) ![}](rbrace.gif) |
17 | | df-rab 2623 |
. . . 4
![{](lbrace.gif) ![E.](exists.gif)
Phi ![y](_y.gif) ![{](lbrace.gif)
![(](lp.gif) ![E.](exists.gif)
Phi ![y](_y.gif) ![)](rp.gif) ![}](rbrace.gif) |
18 | 16, 17 | eqtr4i 2376 |
. . 3
![{](lbrace.gif) ![E.](exists.gif)
Proj1 ![A](_ca.gif) Phi ![y](_y.gif) ![{](lbrace.gif) ![E.](exists.gif) Phi ![y](_y.gif) ![}](rbrace.gif) |
19 | | df-proj2 4568 |
. . . . . . 7
Proj2 ![{](lbrace.gif) Phi 0c![}](rbrace.gif) ![A](_ca.gif) ![}](rbrace.gif) |
20 | 19 | rexeqi 2812 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif)
Proj2 ![A](_ca.gif)
Phi 0c![}](rbrace.gif)
![E.](exists.gif) ![{](lbrace.gif) Phi 0c![}](rbrace.gif)
![A](_ca.gif) ![}](rbrace.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
21 | 4 | uneq1d 3417 |
. . . . . . . 8
![(](lp.gif) Phi 0c![}](rbrace.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 21 | eleq1d 2419 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif) Phi 0c![}](rbrace.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 22 | rexab 2999 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif)
![{](lbrace.gif) Phi 0c![}](rbrace.gif) ![A](_ca.gif) ![}](rbrace.gif)
Phi 0c![}](rbrace.gif)
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
24 | | ancom 437 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif) Phi 0c![}](rbrace.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
25 | | eleq1 2413 |
. . . . . . . . . 10
![(](lp.gif) Phi 0c![}](rbrace.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif) ![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 25 | pm5.32i 618 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) Phi
0c![}](rbrace.gif) ![A](_ca.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif)
Phi 0c![}](rbrace.gif)
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 24, 26 | bitr4i 243 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif)
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 27 | exbii 1582 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
Phi 0c![}](rbrace.gif)
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
29 | | 19.41v 1901 |
. . . . . . 7
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif)
![A](_ca.gif) ![(](lp.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif)
![A](_ca.gif) ![)](rp.gif) ![)](rp.gif) |
30 | | ancom 437 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![A](_ca.gif) ![(](lp.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 28, 29, 30 | 3bitri 262 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Phi 0c![}](rbrace.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 20, 23, 31 | 3bitri 262 |
. . . . 5
![(](lp.gif) ![E.](exists.gif)
Proj2 ![A](_ca.gif)
Phi 0c![}](rbrace.gif)
![(](lp.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | 32 | abbii 2465 |
. . . 4
![{](lbrace.gif) ![E.](exists.gif)
Proj2 ![A](_ca.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![{](lbrace.gif)
![(](lp.gif)
![E.](exists.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
34 | | df-rab 2623 |
. . . 4
![{](lbrace.gif) ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![{](lbrace.gif) ![(](lp.gif) ![E.](exists.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
35 | 33, 34 | eqtr4i 2376 |
. . 3
![{](lbrace.gif) ![E.](exists.gif)
Proj2 ![A](_ca.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![{](lbrace.gif)
![E.](exists.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![}](rbrace.gif) |
36 | 18, 35 | uneq12i 3416 |
. 2
![(](lp.gif) ![{](lbrace.gif)
![E.](exists.gif) Proj1 ![A](_ca.gif)
Phi ![y](_y.gif) ![{](lbrace.gif)
![E.](exists.gif) Proj2 ![A](_ca.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![}](rbrace.gif) ![(](lp.gif) ![{](lbrace.gif) ![E.](exists.gif) Phi ![y](_y.gif) ![{](lbrace.gif) ![E.](exists.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![}](rbrace.gif) ![)](rp.gif) |
37 | | unrab 3526 |
. . 3
![(](lp.gif) ![{](lbrace.gif)
![E.](exists.gif)
Phi ![y](_y.gif) ![{](lbrace.gif) ![E.](exists.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![}](rbrace.gif) ![{](lbrace.gif) ![(](lp.gif) ![E.](exists.gif) Phi ![E.](exists.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
38 | | rabid2 2788 |
. . . 4
![(](lp.gif) ![{](lbrace.gif) ![(](lp.gif) ![E.](exists.gif)
Phi ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![A.](forall.gif) ![(](lp.gif) ![E.](exists.gif)
Phi ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | | vex 2862 |
. . . . . . 7
![_V](rmcv.gif) |
40 | 39 | phiall 4618 |
. . . . . 6
![E.](exists.gif) ![y](_y.gif) ![(](lp.gif)
Phi Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
41 | | 19.43 1605 |
. . . . . 6
![(](lp.gif) ![E.](exists.gif) ![y](_y.gif) ![(](lp.gif) Phi
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![(](lp.gif) ![E.](exists.gif)
Phi ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
42 | 40, 41 | mpbi 199 |
. . . . 5
![(](lp.gif) ![E.](exists.gif)
Phi ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 42 | a1i 10 |
. . . 4
![(](lp.gif) ![(](lp.gif) ![E.](exists.gif)
Phi ![E.](exists.gif)
Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
44 | 38, 43 | mprgbir 2684 |
. . 3
![{](lbrace.gif)
![(](lp.gif) ![E.](exists.gif) Phi ![E.](exists.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![)](rp.gif) ![}](rbrace.gif) |
45 | 37, 44 | eqtr4i 2376 |
. 2
![(](lp.gif) ![{](lbrace.gif)
![E.](exists.gif)
Phi ![y](_y.gif) ![{](lbrace.gif) ![E.](exists.gif) Phi 0c![}](rbrace.gif) ![)](rp.gif) ![}](rbrace.gif) ![A](_ca.gif) |
46 | 1, 36, 45 | 3eqtrri 2378 |
1
Proj1 ![A](_ca.gif) Proj2 ![A](_ca.gif) ![>.](rangle.gif) |