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

Theorem nfeqd 2599
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 2445 . 2  |-  ( A  =  B  <->  A. y
( y  e.  A  <->  y  e.  B ) )
2 nfv 1761 . . 3  |-  F/ y
ph
3 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
43nfcrd 2598 . . . 4  |-  ( ph  ->  F/ x  y  e.  A )
5 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
65nfcrd 2598 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
74, 6nfbid 2016 . . 3  |-  ( ph  ->  F/ x ( y  e.  A  <->  y  e.  B ) )
82, 7nfald 2034 . 2  |-  ( ph  ->  F/ x A. y
( y  e.  A  <->  y  e.  B ) )
91, 8nfxfrd 1697 1  |-  ( ph  ->  F/ x  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   A.wal 1442    = wceq 1444   F/wnf 1667    e. wcel 1887   F/_wnfc 2579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668  df-cleq 2444  df-nfc 2581
This theorem is referenced by:  nfeld  2600  nfeq  2603  nfned  2724  vtoclgft  3096  sbcralt  3340  csbiebt  3383  dfnfc2  4216  eusvnfb  4599  eusv2i  4600  dfid3  4750  nfiotad  5549  iota2df  5570  riota5f  6276  oprabid  6317  axrepndlem1  9017  axrepndlem2  9018  axunnd  9021  axpowndlem4  9025  axregndlem2  9028  axinfndlem1  9030  axinfnd  9031  axacndlem4  9035  axacndlem5  9036  axacnd  9037  riotasv2d  32529  riotaeqimp  39037
  Copyright terms: Public domain W3C validator