Theorem nfcriv

Description: Consequence of the not-free predicate, similiar to nfcri . Requires y and A be disjoint, but is not based on ax-13 . (Contributed by Wolf Lammen, 13-May-2023)

	Ref	Expression
Hypothesis	nfcriv.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfcriv	$$⊢Ⅎxy\in A$$

Proof

Step	Hyp	Ref	Expression
1		nfcriv.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfcr	$$⊢\underset{\_}{Ⅎ}xA\to Ⅎxy\in A$$
3	1 2	ax-mp	$$⊢Ⅎxy\in A$$