Metamath Proof Explorer


Theorem drnfc1OLD

Description: Obsolete version of drnfc1 as of 22-Sep-2024. (Contributed by Mario Carneiro, 8-Oct-2016) Avoid ax-11 . (Revised by Wolf Lammen, 10-May-2023) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis drnfc1.1 ( ∀ 𝑥 𝑥 = 𝑦𝐴 = 𝐵 )
Assertion drnfc1OLD ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 𝐴 𝑦 𝐵 ) )

Proof

Step Hyp Ref Expression
1 drnfc1.1 ( ∀ 𝑥 𝑥 = 𝑦𝐴 = 𝐵 )
2 1 eleq2d ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑤𝐴𝑤𝐵 ) )
3 2 drnf1 ( ∀ 𝑥 𝑥 = 𝑦 → ( Ⅎ 𝑥 𝑤𝐴 ↔ Ⅎ 𝑦 𝑤𝐵 ) )
4 3 albidv ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑤𝑥 𝑤𝐴 ↔ ∀ 𝑤𝑦 𝑤𝐵 ) )
5 df-nfc ( 𝑥 𝐴 ↔ ∀ 𝑤𝑥 𝑤𝐴 )
6 df-nfc ( 𝑦 𝐵 ↔ ∀ 𝑤𝑦 𝑤𝐵 )
7 4 5 6 3bitr4g ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 𝐴 𝑦 𝐵 ) )