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

Theorem nfeqd 2446
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 2290 . 2  |-  ( A  =  B  <->  A. y
( y  e.  A  <->  y  e.  B ) )
2 nfv 1609 . . 3  |-  F/ y
ph
3 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
43nfcrd 2445 . . . 4  |-  ( ph  ->  F/ x  y  e.  A )
5 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
65nfcrd 2445 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
74, 6nfbid 1774 . . 3  |-  ( ph  ->  F/ x ( y  e.  A  <->  y  e.  B ) )
82, 7nfald 1787 . 2  |-  ( ph  ->  F/ x A. y
( y  e.  A  <->  y  e.  B ) )
91, 8nfxfrd 1561 1  |-  ( ph  ->  F/ x  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530   F/wnf 1534    = wceq 1632    e. wcel 1696   F/_wnfc 2419
This theorem is referenced by:  nfeld  2447  nfned  2554  vtoclgft  2847  sbcralt  3076  csbiebt  3130  dfnfc2  3861  dfid3  4326  eusvnfb  4546  eusv2i  4547  nfiotad  5238  iota2df  5259  oprabid  5898  riota5f  6345  riotasvdOLD  6364  riotasv2d  6365  riotasv2dOLD  6366  axrepndlem1  8230  axrepndlem2  8231  axunnd  8234  axpowndlem2  8236  axpowndlem4  8238  axregndlem2  8241  axinfndlem1  8243  axinfnd  8244  axacndlem4  8248  axacndlem5  8249  axacnd  8250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1535  df-cleq 2289  df-nfc 2421
  Copyright terms: Public domain W3C validator