This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfceqi

Description: Equality theorem for class not-free. (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 16-Nov-2019) Avoid ax-12 . (Revised by Wolf Lammen, 19-Jun-2023)

		Ref	Expression
	Hypothesis	nfceqi.1	⊢ 𝐴 = 𝐵
	Assertion	nfceqi	⊢ ( Ⅎ 𝑥 𝐴 ↔ Ⅎ 𝑥 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nfceqi.1	⊢ 𝐴 = 𝐵
2	1	eleq2i	⊢ ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 )
3	2	nfbii	⊢ ( Ⅎ 𝑥 𝑦 ∈ 𝐴 ↔ Ⅎ 𝑥 𝑦 ∈ 𝐵 )
4	3	albii	⊢ ( ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐵 )
5		df-nfc	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )
6		df-nfc	⊢ ( Ⅎ 𝑥 𝐵 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐵 )
7	4 5 6	3bitr4i	⊢ ( Ⅎ 𝑥 𝐴 ↔ Ⅎ 𝑥 𝐵 )