Theorem nfceqdfOLD

Description: Obsolete version of nfceqdf as of 23-Aug-2024. (Contributed by Mario Carneiro, 14-Oct-2016) (Proof modification is discouraged.) (New usage is discouraged.)

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

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	⊢ ( 𝜑 → ( Ⅎ 𝑥 𝐴 ↔ Ⅎ 𝑥 𝐵 ) )