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

Theorem nfeqd 2592
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 2416 . 2  |-  ( A  =  B  <->  A. y
( y  e.  A  <->  y  e.  B ) )
2 nfv 1752 . . 3  |-  F/ y
ph
3 nfeqd.1 . . . . 5  |-  ( ph  -> 
F/_ x A )
43nfcrd 2591 . . . 4  |-  ( ph  ->  F/ x  y  e.  A )
5 nfeqd.2 . . . . 5  |-  ( ph  -> 
F/_ x B )
65nfcrd 2591 . . . 4  |-  ( ph  ->  F/ x  y  e.  B )
74, 6nfbid 1990 . . 3  |-  ( ph  ->  F/ x ( y  e.  A  <->  y  e.  B ) )
82, 7nfald 2008 . 2  |-  ( ph  ->  F/ x A. y
( y  e.  A  <->  y  e.  B ) )
91, 8nfxfrd 1694 1  |-  ( ph  ->  F/ x  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188   A.wal 1436    = wceq 1438   F/wnf 1664    e. wcel 1869   F/_wnfc 2571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1661  df-nf 1665  df-cleq 2415  df-nfc 2573
This theorem is referenced by:  nfeld  2593  nfeq  2596  nfned  2758  vtoclgft  3130  sbcralt  3373  csbiebt  3416  dfnfc2  4235  eusvnfb  4618  eusv2i  4619  dfid3  4767  nfiotad  5566  iota2df  5587  riota5f  6289  oprabid  6330  axrepndlem1  9019  axrepndlem2  9020  axunnd  9023  axpowndlem4  9027  axregndlem2  9030  axinfndlem1  9032  axinfnd  9033  axacndlem4  9037  axacndlem5  9038  axacnd  9039  riotasv2d  32454
  Copyright terms: Public domain W3C validator