Step | Hyp | Ref
| Expression |
1 | | raleq 2629 |
. . . 4
![( (](lp.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![E. E.](exists.gif)
![A. A.](forall.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
2 | | feq2 5264 |
. . . . . 6
![( (](lp.gif)
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif)
![f f](_f.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
3 | | raleq 2629 |
. . . . . 6
![( (](lp.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
4 | 2, 3 | anbi12d 465 |
. . . . 5
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
5 | 4 | exbidv 1798 |
. . . 4
![( (](lp.gif)
![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
6 | 1, 5 | imbi12d 233 |
. . 3
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![E. E.](exists.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | | raleq 2629 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![E. E.](exists.gif)
![A. A.](forall.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
8 | | feq2 5264 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![f
f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif)
![f f](_f.gif) ![: :](colon.gif) ![w
w](_w.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
9 | | raleq 2629 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![A.
A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
10 | 8, 9 | anbi12d 465 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
11 | 10 | exbidv 1798 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
12 | 7, 11 | imbi12d 233 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A. A.](forall.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![E. E.](exists.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | | raleq 2629 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![E. E.](exists.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
14 | | feq2 5264 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif)
![f f](_f.gif) ![: :](colon.gif) ![(
(](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
15 | | raleq 2629 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | 14, 15 | anbi12d 465 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | 16 | exbidv 1798 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
18 | | feq1 5263 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![f
f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif)
![g g](_g.gif) ![: :](colon.gif) ![(
(](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
19 | | vex 2692 |
. . . . . . . . . . 11
![_V
_V](rmcv.gif) |
20 | | vex 2692 |
. . . . . . . . . . 11
![_V
_V](rmcv.gif) |
21 | 19, 20 | fvex 5449 |
. . . . . . . . . 10
![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![_V
_V](rmcv.gif) |
22 | | ac6sfi.1 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
23 | 21, 22 | sbcie 2947 |
. . . . . . . . 9
![( (](lp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
24 | | fveq1 5428 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![f
f](_f.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
25 | 24 | sbceq1d 2918 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | 23, 25 | bitr3id 193 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![[.
[.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | 26 | ralbidv 2438 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
28 | 18, 27 | anbi12d 465 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ps ps](_psi.gif)
![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | 28 | cbvexv 1891 |
. . . . 5
![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![ps ps](_psi.gif) ![E. E.](exists.gif) ![g g](_g.gif) ![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | 17, 29 | syl6bb 195 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![E. E.](exists.gif) ![g g](_g.gif) ![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
31 | 13, 30 | imbi12d 233 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![E. E.](exists.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![g g](_g.gif) ![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
32 | | raleq 2629 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![E. E.](exists.gif)
![A. A.](forall.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
33 | | feq2 5264 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![f
f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif)
![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![-->
-->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
34 | | raleq 2629 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![A.
A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
35 | 33, 34 | anbi12d 465 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
36 | 35 | exbidv 1798 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | 32, 36 | imbi12d 233 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![A. A.](forall.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![u u](_u.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![E. E.](exists.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
38 | | f0 5321 |
. . . 4
![(/) (/)](varnothing.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) |
39 | | 0ex 4063 |
. . . . 5
![_V _V](rmcv.gif) |
40 | | ral0 3469 |
. . . . . . 7
![A. A.](forall.gif) ![ps ps](_psi.gif) |
41 | 40 | biantru 300 |
. . . . . 6
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![--> -->](longrightarrow.gif)
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
42 | | feq1 5263 |
. . . . . 6
![( (](lp.gif)
![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![--> -->](longrightarrow.gif)
![(/) (/)](varnothing.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
43 | 41, 42 | bitr3id 193 |
. . . . 5
![( (](lp.gif)
![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![(/) (/)](varnothing.gif) ![: :](colon.gif) ![(/)
(/)](varnothing.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
44 | 39, 43 | spcev 2784 |
. . . 4
![( (](lp.gif) ![(/) (/)](varnothing.gif) ![: :](colon.gif) ![(/)
(/)](varnothing.gif) ![--> -->](longrightarrow.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
45 | 38, 44 | mp1i 10 |
. . 3
![( (](lp.gif) ![A. A.](forall.gif)
![E. E.](exists.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![(/) (/)](varnothing.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |
46 | | ssun1 3244 |
. . . . . . 7
![( (](lp.gif)
![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
47 | | ssralv 3166 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
48 | 46, 47 | ax-mp 5 |
. . . . . 6
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) |
49 | 48 | imim1i 60 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif) ![)
)](rp.gif) ![) )](rp.gif) |
50 | | ssun2 3245 |
. . . . . . . . 9
![{ {](lbrace.gif) ![z z](_z.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
51 | | ssralv 3166 |
. . . . . . . . 9
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif)
![A. A.](forall.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) ![)
)](rp.gif) |
52 | 50, 51 | ax-mp 5 |
. . . . . . . 8
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) |
53 | | vex 2692 |
. . . . . . . . . 10
![_V
_V](rmcv.gif) |
54 | | ralsnsg 3568 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![E. E.](exists.gif)
![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![E. E.](exists.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
55 | 53, 54 | ax-mp 5 |
. . . . . . . . 9
![( (](lp.gif) ![A. A.](forall.gif)
![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![E. E.](exists.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![) )](rp.gif) |
56 | | sbcrex 2992 |
. . . . . . . . 9
![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![E. E.](exists.gif)
![E. E.](exists.gif)
![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
57 | 55, 56 | bitri 183 |
. . . . . . . 8
![( (](lp.gif) ![A. A.](forall.gif)
![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
58 | 52, 57 | sylib 121 |
. . . . . . 7
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
59 | | nfv 1509 |
. . . . . . . 8
![F/ F/](finv.gif) ![w w](_w.gif) |
60 | | nfv 1509 |
. . . . . . . . 9
![F/ F/](finv.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) |
61 | | nfv 1509 |
. . . . . . . . . . 11
![F/ F/](finv.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) |
62 | | nfcv 2282 |
. . . . . . . . . . . 12
![F/_ F/_](_finvbar.gif) ![y y](_y.gif) ![(
(](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
63 | | nfsbc1v 2931 |
. . . . . . . . . . . 12
![F/ F/](finv.gif) ![y y](_y.gif) ![[.
[.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) |
64 | 62, 63 | nfralxy 2474 |
. . . . . . . . . . 11
![F/ F/](finv.gif) ![y y](_y.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g
g](_g.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) |
65 | 61, 64 | nfan 1545 |
. . . . . . . . . 10
![F/ F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
66 | 65 | nfex 1617 |
. . . . . . . . 9
![F/ F/](finv.gif) ![y y](_y.gif) ![E. E.](exists.gif) ![g g](_g.gif) ![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
67 | 60, 66 | nfim 1552 |
. . . . . . . 8
![F/ F/](finv.gif) ![y y](_y.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![E. E.](exists.gif) ![g g](_g.gif) ![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
68 | | simprl 521 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![f f](_f.gif) ![: :](colon.gif) ![w
w](_w.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) |
69 | | vex 2692 |
. . . . . . . . . . . . . . . 16
![_V
_V](rmcv.gif) |
70 | 53, 69 | f1osn 5415 |
. . . . . . . . . . . . . . 15
![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![: :](colon.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) |
71 | | f1of 5375 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![: :](colon.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![-1-1-onto-> -1-1-onto->](onetooneonto.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![: :](colon.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![--> -->](longrightarrow.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
72 | 70, 71 | mp1i 10 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![: :](colon.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![--> -->](longrightarrow.gif) ![{ {](lbrace.gif) ![y y](_y.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
73 | | simpl2 986 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![B B](_cb.gif) ![) )](rp.gif) |
74 | 73 | snssd 3673 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![{ {](lbrace.gif) ![y y](_y.gif) ![B B](_cb.gif) ![) )](rp.gif) |
75 | 72, 74 | fssd 5293 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![: :](colon.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) |
76 | | simpl1 985 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![w w](_w.gif) ![) )](rp.gif) |
77 | | disjsn 3593 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif)
![w w](_w.gif) ![) )](rp.gif) |
78 | 76, 77 | sylibr 133 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![(/) (/)](varnothing.gif) ![) )](rp.gif) |
79 | | fun2 5304 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![: :](colon.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![(/) (/)](varnothing.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) |
80 | 68, 75, 78, 79 | syl21anc 1216 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) |
81 | | simprr 522 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif) |
82 | | eleq1a 2212 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![( (](lp.gif) ![w w](_w.gif) ![) )](rp.gif) ![) )](rp.gif) |
83 | 82 | necon3bd 2352 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif)
![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
84 | 83 | impcom 124 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif)
![w w](_w.gif)
![x x](_x.gif) ![) )](rp.gif) |
85 | | fvunsng 5622 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![x x](_x.gif) ![(
(](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
86 | 20, 85 | mpan 421 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![(
(](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
87 | | dfsbcq 2915 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(
(](lp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
88 | 87, 23 | syl6rbb 196 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![f f](_f.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(
(](lp.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
89 | 84, 86, 88 | 3syl 17 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif)
![w w](_w.gif)
![( (](lp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
90 | 89 | ralbidva 2434 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![(
(](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
91 | 76, 90 | syl 14 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![A. A.](forall.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
92 | 81, 91 | mpbid 146 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![A. A.](forall.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
93 | | simpl3 987 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
94 | | ffun 5283 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![) )](rp.gif) |
95 | | ssun2 3245 |
. . . . . . . . . . . . . . . . . 18
![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) |
96 | | vsnid 3564 |
. . . . . . . . . . . . . . . . . . 19
![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) |
97 | 69 | dmsnop 5020 |
. . . . . . . . . . . . . . . . . . 19
![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif)
![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) |
98 | 96, 97 | eleqtrri 2216 |
. . . . . . . . . . . . . . . . . 18
![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) |
99 | | funssfv 5455 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![z z](_z.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![` `](backtick.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) |
100 | 95, 98, 99 | mp3an23 1308 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![(
(](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![z z](_z.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![`
`](backtick.gif) ![z z](_z.gif) ![) )](rp.gif) ![)
)](rp.gif) |
101 | 80, 94, 100 | 3syl 17 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![z z](_z.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![` `](backtick.gif) ![z z](_z.gif) ![) )](rp.gif) ![) )](rp.gif) |
102 | 53, 69 | fvsn 5623 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![{ {](lbrace.gif) ![<.
<.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![`
`](backtick.gif) ![z z](_z.gif) ![y y](_y.gif) |
103 | 101, 102 | eqtr2di 2190 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) |
104 | | ralsnsg 3568 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif)
![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
105 | 53, 104 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![A. A.](forall.gif)
![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
106 | | elsni 3550 |
. . . . . . . . . . . . . . . . . . . . 21
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![z z](_z.gif) ![) )](rp.gif) |
107 | 106 | fveq2d 5433 |
. . . . . . . . . . . . . . . . . . . 20
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) |
108 | 107 | eqeq2d 2152 |
. . . . . . . . . . . . . . . . . . 19
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![z z](_z.gif) ![)
)](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
109 | 108 | biimparc 297 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![z z](_z.gif)
![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
110 | | sbceq1a 2922 |
. . . . . . . . . . . . . . . . . 18
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![(
(](lp.gif)
![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
111 | 109, 110 | syl 14 |
. . . . . . . . . . . . . . . . 17
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![z z](_z.gif)
![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![[.
[.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
112 | 111 | ralbidva 2434 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![z z](_z.gif) ![(
(](lp.gif) ![A. A.](forall.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
113 | 105, 112 | bitr3id 193 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![z z](_z.gif) ![(
(](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![(
(](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
114 | 103, 113 | syl 14 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif)
![A. A.](forall.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
115 | 93, 114 | mpbid 146 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![A. A.](forall.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
116 | | ralun 3263 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![A. A.](forall.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![(
(](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
117 | 92, 115, 116 | syl2anc 409 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) |
118 | 53, 69 | opex 4159 |
. . . . . . . . . . . . . . 15
![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![_V _V](rmcv.gif) |
119 | 118 | snex 4117 |
. . . . . . . . . . . . . 14
![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![_V _V](rmcv.gif) |
120 | 19, 119 | unex 4370 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![_V _V](rmcv.gif) |
121 | | feq1 5263 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![g
g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
122 | | fveq1 5428 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![g
g](_g.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![) )](rp.gif) ![) )](rp.gif) |
123 | 122 | sbceq1d 2918 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
124 | 123 | ralbidv 2438 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g
g](_g.gif) ![`
`](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif)
![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
125 | 121, 124 | anbi12d 465 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![( (](lp.gif) ![(
(](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif)
![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>.
>.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
126 | 120, 125 | spcev 2784 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![<. <.](langle.gif) ![z z](_z.gif) ![y y](_y.gif) ![>. >.](rangle.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![E. E.](exists.gif) ![g g](_g.gif) ![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
127 | 80, 117, 126 | syl2anc 409 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![E. E.](exists.gif) ![g g](_g.gif) ![(
(](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) |
128 | 127 | ex 114 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![E. E.](exists.gif) ![g g](_g.gif) ![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
129 | 128 | exlimdv 1792 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![E. E.](exists.gif) ![g g](_g.gif) ![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
130 | 129 | 3exp 1181 |
. . . . . . . 8
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![E. E.](exists.gif) ![g g](_g.gif) ![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
131 | 59, 67, 130 | rexlimd 2549 |
. . . . . . 7
![( (](lp.gif) ![(
(](lp.gif) ![E. E.](exists.gif) ![[. [.](_dlbrack.gif) ![x x](_x.gif) ![]. ].](_drbrack.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![E. E.](exists.gif) ![g g](_g.gif) ![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
132 | 58, 131 | syl5 32 |
. . . . . 6
![( (](lp.gif) ![(
(](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![( (](lp.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![E. E.](exists.gif) ![g g](_g.gif) ![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
133 | 132 | a2d 26 |
. . . . 5
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![g g](_g.gif) ![(
(](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
134 | 49, 133 | syl5 32 |
. . . 4
![( (](lp.gif) ![(
(](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![E. E.](exists.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![(
(](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif)
![ps ps](_psi.gif) ![) )](rp.gif)
![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif) ![E. E.](exists.gif) ![g g](_g.gif) ![( (](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{
{](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z
z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
135 | 134 | adantl 275 |
. . 3
![( (](lp.gif) ![( (](lp.gif)
![w w](_w.gif)
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![E. E.](exists.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![w w](_w.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![E. E.](exists.gif)
![E. E.](exists.gif) ![g g](_g.gif) ![(
(](lp.gif) ![g g](_g.gif) ![: :](colon.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![( (](lp.gif) ![{ {](lbrace.gif) ![z z](_z.gif) ![} }](rbrace.gif) ![) )](rp.gif) ![[. [.](_dlbrack.gif) ![( (](lp.gif) ![g g](_g.gif) ![` `](backtick.gif) ![x x](_x.gif) ![y
y](_y.gif) ![]. ].](_drbrack.gif) ![ph ph](_varphi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
136 | 6, 12, 31, 37, 45, 135 | findcard2s 6792 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif)
![E. E.](exists.gif)
![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) ![) )](rp.gif) |
137 | 136 | imp 123 |
1
![( (](lp.gif) ![( (](lp.gif) ![A. A.](forall.gif) ![E. E.](exists.gif)
![ph ph](_varphi.gif) ![E. E.](exists.gif) ![f f](_f.gif) ![( (](lp.gif) ![f f](_f.gif) ![: :](colon.gif) ![A A](_ca.gif) ![--> -->](longrightarrow.gif) ![A. A.](forall.gif) ![ps ps](_psi.gif) ![) )](rp.gif) ![) )](rp.gif) |