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 x x = y A = B
Assertion drnfc1OLD x x = y _ x A _ y B

Proof

Step Hyp Ref Expression
1 drnfc1.1 x x = y A = B
2 1 eleq2d x x = y w A w B
3 2 drnf1 x x = y x w A y w B
4 3 albidv x x = y w x w A w y w B
5 df-nfc _ x A w x w A
6 df-nfc _ y B w y w B
7 4 5 6 3bitr4g x x = y _ x A _ y B