Metamath Proof Explorer


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