Theorem nfcriOLDOLD

Description: Obsolete version of nfcri as of 26-May-2024. (Contributed by Mario Carneiro, 11-Aug-2016) Avoid ax-10 , ax-11 . (Revised by Gino Giotto, 23-May-2024) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		nfcrii.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		eleq1w	$$⊢z=y\to \left(z\in A\leftrightarrow y\in A\right)$$
3	2	nfbidv	$$⊢z=y\to \left(Ⅎxz\in A\leftrightarrow Ⅎxy\in A\right)$$
4		df-nfc	$$⊢\underset{\_}{Ⅎ}xA\leftrightarrow \forall zℲxz\in A$$
5	4	biimpi	$$⊢\underset{\_}{Ⅎ}xA\to \forall zℲxz\in A$$
6		df-nf	$$⊢Ⅎxz\in A\leftrightarrow \left(\exists xz\in A\to \forall xz\in A\right)$$
7	6	albii	$$⊢\forall zℲxz\in A\leftrightarrow \forall z\left(\exists xz\in A\to \forall xz\in A\right)$$
8		sp	$$⊢\forall z\left(\exists xz\in A\to \forall xz\in A\right)\to \left(\exists xz\in A\to \forall xz\in A\right)$$
9	7 8	sylbi	$$⊢\forall zℲxz\in A\to \left(\exists xz\in A\to \forall xz\in A\right)$$
10	1 5 9	mp2b	$$⊢\exists xz\in A\to \forall xz\in A$$
11	10	nfi	$$⊢Ⅎxz\in A$$
12	3 11	chvarvv	$$⊢Ⅎxy\in A$$