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

Theorem nfeq 2578
Description: Hypothesis builder for equality. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypotheses
Ref Expression
nfnfc.1  |-  F/_ x A
nfeq.2  |-  F/_ x B
Assertion
Ref Expression
nfeq  |-  F/ x  A  =  B

Proof of Theorem nfeq
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2429 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2565 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2565 . . . 4  |-  F/ x  z  e.  B
63, 5nfbi 1856 . . 3  |-  F/ x
( z  e.  A  <->  z  e.  B )
76nfal 1864 . 2  |-  F/ x A. z ( z  e.  A  <->  z  e.  B
)
81, 7nfxfr 1579 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1549   F/wnf 1553    = wceq 1652    e. wcel 1725   F/_wnfc 2558
This theorem is referenced by:  nfel  2579  nfeq1  2580  nfeq2  2582  nfne  2689  raleqf  2892  rexeqf  2893  reueq1f  2894  rmoeq1f  2895  rabeqf  2941  sbceqg  3259  csbhypf  3278  nffn  5532  nffo  5643  fvmptdf  5807  mpteqb  5810  fvmptf  5812  eqfnfv2f  5822  dff13f  5997  ovmpt2s  6188  ov2gf  6189  ovmpt2dxf  6190  ovmpt2df  6196  eqerlem  6928  seqof2  11369  sumeq1f  12470  sumeq2w  12474  sumeq2ii  12475  sumss  12506  fsumadd  12520  fsummulc2  12555  fsumrelem  12574  txcnp  17640  ptcnplem  17641  cnmpt11  17683  cnmpt21  17691  cnmptcom  17698  mbfeqalem  19522  mbflim  19548  itgeq1f  19651  itgeqa  19693  dvmptfsum  19847  ulmss  20301  leibpi  20770  o1cxp  20801  lgseisenlem2  21122  prodeq1f  25223  prodeq2w  25227  prodeq2ii  25228  fprodmul  25273  fproddiv  25274  subtr  26254  subtr2  26255  dvdsrabdioph  26807  fphpd  26814  fvelrnbf  27603  refsum2cnlem1  27622  fmuldfeq  27627  climmulf  27644  climexp  27645  climsuse  27648  climrecf  27649  stoweidlem18  27681  stoweidlem31  27694  stoweidlem55  27718  stoweidlem59  27722  bnj1316  29046  bnj1446  29268  bnj1447  29269  bnj1448  29270  bnj1519  29288  bnj1520  29289  bnj1529  29293
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2428  df-clel 2431  df-nfc 2560
  Copyright terms: Public domain W3C validator