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

Theorem nfeqd 2623
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 2447 . 2  |-  ( A  =  B  <->  A. y
( y  e.  A  <->  y  e.  B ) )
2 nfv 1674 . . 3  |-  F/ y
ph
3 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
43nfcrd 2622 . . . 4  |-  ( ph  ->  F/ x  y  e.  A )
5 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
65nfcrd 2622 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
74, 6nfbid 1871 . . 3  |-  ( ph  ->  F/ x ( y  e.  A  <->  y  e.  B ) )
82, 7nfald 1889 . 2  |-  ( ph  ->  F/ x A. y
( y  e.  A  <->  y  e.  B ) )
91, 8nfxfrd 1617 1  |-  ( ph  ->  F/ x  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1368    = wceq 1370   F/wnf 1590    e. wcel 1758   F/_wnfc 2602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-cleq 2446  df-nfc 2604
This theorem is referenced by:  nfeld  2624  nfeq  2627  nfned  2784  vtoclgft  3126  sbcralt  3375  csbiebt  3418  dfnfc2  4220  eusvnfb  4599  eusv2i  4600  dfid3  4748  nfiotad  5495  iota2df  5516  riota5f  6189  oprabid  6227  axrepndlem1  8870  axrepndlem2  8871  axunnd  8874  axpowndlem2OLD  8877  axpowndlem4  8880  axregndlem2  8883  axinfndlem1  8886  axinfnd  8887  axacndlem4  8891  axacndlem5  8892  axacnd  8893  riotasv2d  32966
  Copyright terms: Public domain W3C validator