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

Theorem nfeqd 2619
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 2465 . 2  |-  ( A  =  B  <->  A. y
( y  e.  A  <->  y  e.  B ) )
2 nfv 1769 . . 3  |-  F/ y
ph
3 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
43nfcrd 2618 . . . 4  |-  ( ph  ->  F/ x  y  e.  A )
5 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
65nfcrd 2618 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
74, 6nfbid 2036 . . 3  |-  ( ph  ->  F/ x ( y  e.  A  <->  y  e.  B ) )
82, 7nfald 2053 . 2  |-  ( ph  ->  F/ x A. y
( y  e.  A  <->  y  e.  B ) )
91, 8nfxfrd 1705 1  |-  ( ph  ->  F/ x  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   A.wal 1450    = wceq 1452   F/wnf 1675    e. wcel 1904   F/_wnfc 2599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676  df-cleq 2464  df-nfc 2601
This theorem is referenced by:  nfeld  2620  nfeq  2623  nfned  2743  vtoclgft  3082  sbcralt  3328  csbiebt  3369  dfnfc2  4208  eusvnfb  4597  eusv2i  4598  dfid3  4755  nfiotad  5556  iota2df  5577  riota5f  6294  oprabid  6335  axrepndlem1  9035  axrepndlem2  9036  axunnd  9039  axpowndlem4  9043  axregndlem2  9046  axinfndlem1  9048  axinfnd  9049  axacndlem4  9053  axacndlem5  9054  axacnd  9055  riotasv2d  32593  riotaeqimp  39183
  Copyright terms: Public domain W3C validator