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
|- ( A. x x = y -> A = B )
Assertion drnfc1OLD
|- ( A. x x = y -> ( F/_ x A <-> F/_ y B ) )

Proof

Step Hyp Ref Expression
1 drnfc1.1
 |-  ( A. x x = y -> A = B )
2 1 eleq2d
 |-  ( A. x x = y -> ( w e. A <-> w e. B ) )
3 2 drnf1
 |-  ( A. x x = y -> ( F/ x w e. A <-> F/ y w e. B ) )
4 3 albidv
 |-  ( A. x x = y -> ( A. w F/ x w e. A <-> A. w F/ y w e. B ) )
5 df-nfc
 |-  ( F/_ x A <-> A. w F/ x w e. A )
6 df-nfc
 |-  ( F/_ y B <-> A. w F/ y w e. B )
7 4 5 6 3bitr4g
 |-  ( A. x x = y -> ( F/_ x A <-> F/_ y B ) )