Theorem nfccdeq

Description: Variation of nfcdeq for classes. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Mario Carneiro, 11-Aug-2016) Avoid ax-11 . (Revised by GG, 19-May-2023) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfccdeq.1	|- F/_ x A
	nfccdeq.2	|- CondEq ( x = y -> A = B )
Assertion	nfccdeq	|- A = B

Proof

Step	Hyp	Ref	Expression
1		nfccdeq.1	|- F/_ x A
2		nfccdeq.2	|- CondEq ( x = y -> A = B )
3	1	nfcri	|- F/ x z e. A
4		eqid	|- z = z
5	4	cdeqth	|- CondEq ( x = y -> z = z )
6	5 2	cdeqel	|- CondEq ( x = y -> ( z e. A <-> z e. B ) )
7	3 6	nfcdeq	|- ( z e. A <-> z e. B )
8	7	eqriv	|- A = B