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 1712 . . 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 1938 . . 3  |-  ( ph  ->  F/ x ( y  e.  A  <->  y  e.  B ) )
82, 7nfald 1956 . 2  |-  ( ph  ->  F/ x A. y
( y  e.  A  <->  y  e.  B ) )
91, 8nfxfrd 1651 1  |-  ( ph  ->  F/ x  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1396    = wceq 1398   F/wnf 1621    e. wcel 1823   F/_wnfc 2602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622  df-cleq 2446  df-nfc 2604
This theorem is referenced by:  nfeld  2624  nfeq  2627  nfned  2786  vtoclgft  3154  sbcralt  3397  csbiebt  3440  dfnfc2  4253  eusvnfb  4633  eusv2i  4634  dfid3  4785  nfiotad  5537  iota2df  5558  riota5f  6256  oprabid  6297  axrepndlem1  8958  axrepndlem2  8959  axunnd  8962  axpowndlem4  8966  axregndlem2  8969  axinfndlem1  8972  axinfnd  8973  axacndlem4  8977  axacndlem5  8978  axacnd  8979  riotasv2d  35085
  Copyright terms: Public domain W3C validator