Theorem nfceqdf

Description: An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016) Avoid ax-8 and df-clel . (Revised by WL and SN, 23-Aug-2024)

	Ref	Expression
Hypotheses	nfceqdf.1	⊢ Ⅎ 𝑥 𝜑
	nfceqdf.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	nfceqdf	⊢ ( 𝜑 → ( Ⅎ 𝑥 𝐴 ↔ Ⅎ 𝑥 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nfceqdf.1	⊢ Ⅎ 𝑥 𝜑
2		nfceqdf.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3		eleq2w2	⊢ ( 𝐴 = 𝐵 → ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
4	2 3	syl	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ 𝐵 ) )
5	1 4	nfbidf	⊢ ( 𝜑 → ( Ⅎ 𝑥 𝑦 ∈ 𝐴 ↔ Ⅎ 𝑥 𝑦 ∈ 𝐵 ) )
6	5	albidv	⊢ ( 𝜑 → ( ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐵 ) )
7		df-nfc	⊢ ( Ⅎ 𝑥 𝐴 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐴 )
8		df-nfc	⊢ ( Ⅎ 𝑥 𝐵 ↔ ∀ 𝑦 Ⅎ 𝑥 𝑦 ∈ 𝐵 )
9	6 7 8	3bitr4g	⊢ ( 𝜑 → ( Ⅎ 𝑥 𝐴 ↔ Ⅎ 𝑥 𝐵 ) )