MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfeqd Structured version   Unicode version

Theorem nfeqd 2636
Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 7-Oct-2016.)
Hypotheses
Ref Expression
nfeqd.1  |-  ( ph  -> 
F/_ x A )
nfeqd.2  |-  ( ph  -> 
F/_ x B )
Assertion
Ref Expression
nfeqd  |-  ( ph  ->  F/ x  A  =  B )

Proof of Theorem nfeqd
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2460 . 2  |-  ( A  =  B  <->  A. y
( y  e.  A  <->  y  e.  B ) )
2 nfv 1683 . . 3  |-  F/ y
ph
3 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
43nfcrd 2635 . . . 4  |-  ( ph  ->  F/ x  y  e.  A )
5 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
65nfcrd 2635 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
74, 6nfbid 1880 . . 3  |-  ( ph  ->  F/ x ( y  e.  A  <->  y  e.  B ) )
82, 7nfald 1898 . 2  |-  ( ph  ->  F/ x A. y
( y  e.  A  <->  y  e.  B ) )
91, 8nfxfrd 1626 1  |-  ( ph  ->  F/ x  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1377    = wceq 1379   F/wnf 1599    e. wcel 1767   F/_wnfc 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600  df-cleq 2459  df-nfc 2617
This theorem is referenced by:  nfeld  2637  nfeq  2640  nfned  2799  vtoclgft  3161  sbcralt  3412  csbiebt  3455  dfnfc2  4263  eusvnfb  4643  eusv2i  4644  dfid3  4796  nfiotad  5554  iota2df  5575  riota5f  6271  oprabid  6309  axrepndlem1  8968  axrepndlem2  8969  axunnd  8972  axpowndlem2OLD  8975  axpowndlem4  8978  axregndlem2  8981  axinfndlem1  8984  axinfnd  8985  axacndlem4  8989  axacndlem5  8990  axacnd  8991  riotasv2d  33977
  Copyright terms: Public domain W3C validator