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	|- F/_ x A
Assertion	nfcriOLD	|- F/ x y e. A

Proof

Step	Hyp	Ref	Expression
1		nfcrii.1	|- F/_ x A
2		eleq1w	|- ( z = y -> ( z e. A <-> y e. A ) )
3	2	nfbidv	|- ( z = y -> ( F/ x z e. A <-> F/ x y e. A ) )
4		df-nfc	|- ( F/_ x A <-> A. z F/ x z e. A )
5	4	biimpi	|- ( F/_ x A -> A. z F/ x z e. A )
6		df-nf	|- ( F/ x z e. A <-> ( E. x z e. A -> A. x z e. A ) )
7	6	albii	|- ( A. z F/ x z e. A <-> A. z ( E. x z e. A -> A. x z e. A ) )
8		eleq1w	|- ( z = w -> ( z e. A <-> w e. A ) )
9	8	exbidv	|- ( z = w -> ( E. x z e. A <-> E. x w e. A ) )
10	8	albidv	|- ( z = w -> ( A. x z e. A <-> A. x w e. A ) )
11	9 10	imbi12d	|- ( z = w -> ( ( E. x z e. A -> A. x z e. A ) <-> ( E. x w e. A -> A. x w e. A ) ) )
12	11	spw	|- ( A. z ( E. x z e. A -> A. x z e. A ) -> ( E. x z e. A -> A. x z e. A ) )
13	7 12	sylbi	|- ( A. z F/ x z e. A -> ( E. x z e. A -> A. x z e. A ) )
14	1 5 13	mp2b	|- ( E. x z e. A -> A. x z e. A )
15	14	nfi	|- F/ x z e. A
16	3 15	chvarvv	|- F/ x y e. A