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
|- F/ x ph
nfceqdf.2
|- ( ph -> A = B )
Assertion nfceqdfOLD
|- ( ph -> ( F/_ x A <-> F/_ x B ) )

Proof

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