fv-exy
Theorem.
Arguments:
(sv),
(sv),
(pr),
Hypotheses:
(
)
Assertions:
(
)
Proof:
Hyp
Ref
Line
Expr
Hypo
1
(
)
1
fv-neg
2
(
)
2
fv-aly
3
(
)
3
fv-neg
4
(
)
df-ex
5
(
)
5
eqt-∀-i
6
(
)
4, 5, 6
<imtr
7
(
)