Theorem nfcriOLD

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

	Ref	Expression
Hypothesis	nfcrii.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfcriOLD	$$⊢Ⅎ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		eleq1w	$$⊢z=w\to \left(z\in A\leftrightarrow w\in A\right)$$
9	8	exbidv	$$⊢z=w\to \left(\exists xz\in A\leftrightarrow \exists xw\in A\right)$$
10	8	albidv	$$⊢z=w\to \left(\forall xz\in A\leftrightarrow \forall xw\in A\right)$$
11	9 10	imbi12d	$$⊢z=w\to \left(\left(\exists xz\in A\to \forall xz\in A\right)\leftrightarrow \left(\exists xw\in A\to \forall xw\in A\right)\right)$$
12	11	spw	$$⊢\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)$$
13	7 12	sylbi	$$⊢\forall zℲxz\in A\to \left(\exists xz\in A\to \forall xz\in A\right)$$
14	1 5 13	mp2b	$$⊢\exists xz\in A\to \forall xz\in A$$
15	14	nfi	$$⊢Ⅎxz\in A$$
16	3 15	chvarvv	$$⊢Ⅎxy\in A$$