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

Theorem nfeqd 2433
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 2277 . 2  |-  ( A  =  B  <->  A. y
( y  e.  A  <->  y  e.  B ) )
2 nfv 1605 . . 3  |-  F/ y
ph
3 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
43nfcrd 2432 . . . 4  |-  ( ph  ->  F/ x  y  e.  A )
5 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
65nfcrd 2432 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
74, 6nfbid 1762 . . 3  |-  ( ph  ->  F/ x ( y  e.  A  <->  y  e.  B ) )
82, 7nfald 1775 . 2  |-  ( ph  ->  F/ x A. y
( y  e.  A  <->  y  e.  B ) )
91, 8nfxfrd 1558 1  |-  ( ph  ->  F/ x  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527   F/wnf 1531    = wceq 1623    e. wcel 1684   F/_wnfc 2406
This theorem is referenced by:  nfeld  2434  nfned  2541  vtoclgft  2834  sbcralt  3063  csbiebt  3117  dfnfc2  3845  dfid3  4310  eusvnfb  4530  eusv2i  4531  nfiotad  5222  iota2df  5243  oprabid  5882  riota5f  6329  riotasvdOLD  6348  riotasv2d  6349  riotasv2dOLD  6350  axrepndlem1  8214  axrepndlem2  8215  axunnd  8218  axpowndlem2  8220  axpowndlem4  8222  axregndlem2  8225  axinfndlem1  8227  axinfnd  8228  axacndlem4  8232  axacndlem5  8233  axacnd  8234
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532  df-cleq 2276  df-nfc 2408
  Copyright terms: Public domain W3C validator