Theorem nfcriiOLD

Description: Obsolete version of nfcrii as of 23-May-2024. (Contributed by Mario Carneiro, 11-Aug-2016) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	nfcriOLD.1	|- F/_ x A
Assertion	nfcriiOLD	|- ( y e. A -> A. x y e. A )

Proof

Step	Hyp	Ref	Expression
1		nfcriOLD.1	|- F/_ x A
2	1	nfcri	|- F/ x z e. A
3	2	nfsbv	|- F/ x [ y / z ] z e. A
4	3	nf5ri	|- ( [ y / z ] z e. A -> A. x [ y / z ] z e. A )
5		clelsb1	|- ( [ y / z ] z e. A <-> y e. A )
6	5	albii	|- ( A. x [ y / z ] z e. A <-> A. x y e. A )
7	4 5 6	3imtr3i	|- ( y e. A -> A. x y e. A )