Metamath Proof Explorer


Theorem nfeqd

Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016)

Ref Expression
Hypotheses nfeqd.1
|- ( ph -> F/_ x A )
nfeqd.2
|- ( ph -> F/_ x B )
Assertion nfeqd
|- ( ph -> F/ x A = B )

Proof

Step Hyp Ref Expression
1 nfeqd.1
 |-  ( ph -> F/_ x A )
2 nfeqd.2
 |-  ( ph -> F/_ x B )
3 dfcleq
 |-  ( A = B <-> A. y ( y e. A <-> y e. B ) )
4 nfv
 |-  F/ y ph
5 df-nfc
 |-  ( F/_ x A <-> A. y F/ x y e. A )
6 1 5 sylib
 |-  ( ph -> A. y F/ x y e. A )
7 6 19.21bi
 |-  ( ph -> F/ x y e. A )
8 df-nfc
 |-  ( F/_ x B <-> A. y F/ x y e. B )
9 2 8 sylib
 |-  ( ph -> A. y F/ x y e. B )
10 9 19.21bi
 |-  ( ph -> F/ x y e. B )
11 7 10 nfbid
 |-  ( ph -> F/ x ( y e. A <-> y e. B ) )
12 4 11 nfald
 |-  ( ph -> F/ x A. y ( y e. A <-> y e. B ) )
13 3 12 nfxfrd
 |-  ( ph -> F/ x A = B )