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 Gino Giotto, 19-May-2023) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfccdeq.1	⊢ Ⅎ 𝑥 𝐴
	nfccdeq.2	⊢ CondEq ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
Assertion	nfccdeq	⊢ 𝐴 = 𝐵

Proof

Step	Hyp	Ref	Expression
1		nfccdeq.1	⊢ Ⅎ 𝑥 𝐴
2		nfccdeq.2	⊢ CondEq ( 𝑥 = 𝑦 → 𝐴 = 𝐵 )
3	1	nfcri	⊢ Ⅎ 𝑥 𝑧 ∈ 𝐴
4		eqid	⊢ 𝑧 = 𝑧
5	4	cdeqth	⊢ CondEq ( 𝑥 = 𝑦 → 𝑧 = 𝑧 )
6	5 2	cdeqel	⊢ CondEq ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵 ) )
7	3 6	nfcdeq	⊢ ( 𝑧 ∈ 𝐴 ↔ 𝑧 ∈ 𝐵 )
8	7	eqriv	⊢ 𝐴 = 𝐵