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	$$⊢\underset{\_}{Ⅎ}xA$$
	nfccdeq.2	$$⊢CondEq\left(x=y\to A=B\right)$$
Assertion	nfccdeq	$$⊢A=B$$

Proof

Step	Hyp	Ref	Expression
1		nfccdeq.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		nfccdeq.2	$$⊢CondEq\left(x=y\to A=B\right)$$
3	1	nfcri	$$⊢Ⅎxz\in A$$
4		eqid	$$⊢z=z$$
5	4	cdeqth	$$⊢CondEq\left(x=y\to z=z\right)$$
6	5 2	cdeqel	$$⊢CondEq\left(x=y\to \left(z\in A\leftrightarrow z\in B\right)\right)$$
7	3 6	nfcdeq	$$⊢z\in A\leftrightarrow z\in B$$
8	7	eqriv	$$⊢A=B$$