df-∃1
Definition.
Arguments:
(sv),
(pr),
(sv),
Distinct variable conditions:
(
,
), (
,
),
Assertions:
(
(
(
)))
(sv), 
(pr), 
(sv), (sv), (pr), (sv), , ), (, ), 
((
)))