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

Theorem nfeq 2428
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 2279 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2415 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2415 . . . 4  |-  F/ x  z  e.  B
63, 5nfbi 1774 . . 3  |-  F/ x
( z  e.  A  <->  z  e.  B )
76nfal 1768 . 2  |-  F/ x A. z ( z  e.  A  <->  z  e.  B
)
81, 7nfxfr 1559 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1529   F/wnf 1533    = wceq 1625    e. wcel 1686   F/_wnfc 2408
This theorem is referenced by:  nfel  2429  nfeq1  2430  nfeq2  2432  nfne  2541  raleqf  2734  rexeqf  2735  reueq1f  2736  rmoeq1f  2737  rabeqf  2783  sbceqg  3099  csbhypf  3118  nffn  5342  nffo  5452  fvmptdf  5613  mpteqb  5616  fvmptf  5618  eqfnfv2f  5628  dff13f  5786  ovmpt2s  5973  ov2gf  5974  ovmpt2dxf  5975  ovmpt2df  5981  opabiota  6295  eqerlem  6694  sumeq1f  12163  sumeq2w  12167  sumeq2ii  12168  sumss  12199  fsumadd  12213  fsummulc2  12248  fsumrelem  12267  txcnp  17316  ptcnplem  17317  cnmpt11  17359  cnmpt21  17367  cnmptcom  17374  mbfeqalem  18999  mbflim  19025  itgeq1f  19128  itgeqa  19170  dvmptfsum  19324  ulmss  19776  leibpi  20240  o1cxp  20271  lgseisenlem2  20591  dfimafnf  23043  disjabrex  23361  disjabrexf  23362  iundisjf  23367  prodeq3ii  25319  fprodadd  25363  fprodneg  25389  fprodsub  25390  subtr  26235  subtr2  26236  dvdsrabdioph  26902  fphpd  26910  fvelrnbf  27700  refsum2cnlem1  27719  fmuldfeqlem1  27723  fmuldfeq  27724  climmulf  27741  climexp  27742  climsuse  27745  climrecf  27746  stoweidlem8  27768  stoweidlem16  27776  stoweidlem18  27778  stoweidlem19  27779  stoweidlem21  27781  stoweidlem22  27782  stoweidlem23  27783  stoweidlem28  27788  stoweidlem29  27789  stoweidlem31  27791  stoweidlem32  27792  stoweidlem35  27795  stoweidlem36  27796  stoweidlem41  27801  stoweidlem44  27804  stoweidlem45  27805  stoweidlem48  27808  stoweidlem51  27811  stoweidlem53  27813  stoweidlem55  27815  stoweidlem58  27818  stoweidlem59  27819  stoweidlem60  27820  bnj1316  28926  bnj1446  29148  bnj1447  29149  bnj1448  29150  bnj1519  29168  bnj1520  29169  bnj1529  29173
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-cleq 2278  df-clel 2281  df-nfc 2410
  Copyright terms: Public domain W3C validator