Detailed syntax breakdown of Definition df-ex
Step | Hyp | Ref
| Expression |
1 | | kt 8 |
. 2
term ![T.](top.gif) |
2 | | tex 123 |
. . 3
term ![E.](exists.gif) |
3 | | hal |
. . . . 5
type ![al](_alpha.gif) |
4 | | hb 3 |
. . . . 5
type ![*](hexstar.gif) |
5 | 3, 4 | ht 2 |
. . . 4
type ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) |
6 | | vp |
. . . 4
var ![p](_p.gif) |
7 | | tal 122 |
. . . . 5
term ![A.](forall.gif) |
8 | | vq |
. . . . . 6
var ![q](_q.gif) |
9 | | vx |
. . . . . . . . 9
var ![x](_x.gif) |
10 | 5, 6 | tv 1 |
. . . . . . . . . . 11
term ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) |
11 | 3, 9 | tv 1 |
. . . . . . . . . . 11
term ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) |
12 | 10, 11 | kc 5 |
. . . . . . . . . 10
term ![(](lp.gif) ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![)](rp.gif) |
13 | 4, 8 | tv 1 |
. . . . . . . . . 10
term ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) |
14 | | tim 121 |
. . . . . . . . . 10
term ![==>](bigto.gif) |
15 | 12, 13, 14 | kbr 9 |
. . . . . . . . 9
term ![[](lbrack.gif) ![(](lp.gif) ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) |
16 | 3, 9, 15 | kl 6 |
. . . . . . . 8
term ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) |
17 | 7, 16 | kc 5 |
. . . . . . 7
term ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) ![)](rp.gif) |
18 | 17, 13, 14 | kbr 9 |
. . . . . 6
term ![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) |
19 | 4, 8, 18 | kl 6 |
. . . . 5
term ![\](lambda.gif) ![q](_q.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) |
20 | 7, 19 | kc 5 |
. . . 4
term ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![q](_q.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) ![)](rp.gif) |
21 | 5, 6, 20 | kl 6 |
. . 3
term ![\](lambda.gif) ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![q](_q.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) ![)](rp.gif) |
22 | | ke 7 |
. . 3
term ![=](eq.gif) |
23 | 2, 21, 22 | kbr 9 |
. 2
term ![[](lbrack.gif)
![\](lambda.gif) ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![q](_q.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) ![)](rp.gif) ![]](rbrack.gif) |
24 | 1, 23 | wffMMJ2 11 |
1
wff ![[](lbrack.gif) ![\](lambda.gif) ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![q](_q.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![A.](forall.gif) ![\](lambda.gif) ![x](_x.gif) ![:](colon.gif) ![[](lbrack.gif) ![(](lp.gif) ![p](_p.gif) ![:](colon.gif) ![(](lp.gif) ![*](hexstar.gif) ![)](rp.gif) ![x](_x.gif) ![:](colon.gif) ![al](_alpha.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) ![q](_q.gif) ![:](colon.gif) ![*](hexstar.gif) ![]](rbrack.gif) ![)](rp.gif) ![]](rbrack.gif) |