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

Theorem nfeqd 2586
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 2430 . 2  |-  ( A  =  B  <->  A. y
( y  e.  A  <->  y  e.  B ) )
2 nfv 1629 . . 3  |-  F/ y
ph
3 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
43nfcrd 2585 . . . 4  |-  ( ph  ->  F/ x  y  e.  A )
5 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
65nfcrd 2585 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
74, 6nfbid 1854 . . 3  |-  ( ph  ->  F/ x ( y  e.  A  <->  y  e.  B ) )
82, 7nfald 1871 . 2  |-  ( ph  ->  F/ x A. y
( y  e.  A  <->  y  e.  B ) )
91, 8nfxfrd 1580 1  |-  ( ph  ->  F/ x  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549   F/wnf 1553    = wceq 1652    e. wcel 1725   F/_wnfc 2559
This theorem is referenced by:  nfeld  2587  nfned  2696  vtoclgft  3002  sbcralt  3233  csbiebt  3287  dfnfc2  4033  dfid3  4499  eusvnfb  4719  eusv2i  4720  nfiotad  5421  iota2df  5442  oprabid  6105  riota5f  6574  riotasvdOLD  6593  riotasv2d  6594  riotasv2dOLD  6595  axrepndlem1  8467  axrepndlem2  8468  axunnd  8471  axpowndlem2  8473  axpowndlem4  8475  axregndlem2  8478  axinfndlem1  8480  axinfnd  8481  axacndlem4  8485  axacndlem5  8486  axacnd  8487
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-cleq 2429  df-nfc 2561
  Copyright terms: Public domain W3C validator