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	|- F/_ x A
Assertion	nfcriOLDOLD	|- 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		sp	|- ( A. z ( E. x z e. A -> A. x z e. A ) -> ( E. x z e. A -> A. x z e. A ) )
9	7 8	sylbi	|- ( A. z F/ x z e. A -> ( E. x z e. A -> A. x z e. A ) )
10	1 5 9	mp2b	|- ( E. x z e. A -> A. x z e. A )
11	10	nfi	|- F/ x z e. A
12	3 11	chvarvv	|- F/ x y e. A