Theorem nfceqdf

Description: An equality theorem for effectively not free. (Contributed by Mario Carneiro, 14-Oct-2016)

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

Proof

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