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

Theorem nfeq 2399
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
StepHypRef Expression
1 dfcleq 2250 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2386 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2386 . . . 4  |-  F/ x  z  e.  B
63, 5nfbi 1738 . . 3  |-  F/ x
( z  e.  A  <->  z  e.  B )
76nfal 1732 . 2  |-  F/ x A. z ( z  e.  A  <->  z  e.  B
)
81, 7nfxfr 1562 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 178   A.wal 1532   F/wnf 1539    = wceq 1619    e. wcel 1621   F/_wnfc 2379
This theorem is referenced by:  nfel  2400  nfeq1  2401  nfeq2  2403  nfne  2512  raleqf  2705  rexeqf  2706  reueq1f  2707  rabeqf  2750  sbceqg  3058  csbhypf  3077  nffn  5264  nffo  5374  fvmptdf  5531  mpteqb  5534  fvmptf  5536  eqfnfv2f  5546  dff13f  5704  ovmpt2s  5891  ov2gf  5892  ovmpt2dxf  5893  ovmpt2df  5899  opabiota  6245  eqerlem  6646  sumeq1f  12112  sumeq2w  12116  sumeq2ii  12117  sumss  12148  fsumadd  12162  fsummulc2  12197  fsumrelem  12216  txcnp  17262  ptcnplem  17263  cnmpt11  17305  cnmpt21  17313  cnmptcom  17320  mbfeqalem  18945  mbflim  18971  itgeq1f  19074  itgeqa  19116  dvmptfsum  19270  ulmss  19722  leibpi  20186  o1cxp  20217  lgseisenlem2  20537  dfimafnf  22988  prodeq3ii  24661  fprodadd  24705  fprodneg  24731  fprodsub  24732  subtr  25577  subtr2  25578  dvdsrabdioph  26244  fphpd  26252  fvelrnbf  27043  refsum2cnlem1  27062  fmuldfeqlem1  27066  fmuldfeq  27067  stoweidlem8  27078  stoweidlem16  27086  stoweidlem18  27088  stoweidlem19  27089  stoweidlem21  27091  stoweidlem22  27092  stoweidlem23  27093  stoweidlem28  27098  stoweidlem29  27099  stoweidlem31  27101  stoweidlem32  27102  stoweidlem35  27105  stoweidlem36  27106  stoweidlem41  27111  stoweidlem44  27114  stoweidlem45  27115  stoweidlem48  27118  stoweidlem51  27121  stoweidlem53  27123  stoweidlem55  27125  stoweidlem58  27128  stoweidlem59  27129  stoweidlem60  27130  bnj1316  27886  bnj1446  28108  bnj1447  28109  bnj1448  28110  bnj1519  28128  bnj1520  28129  bnj1529  28133
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-cleq 2249  df-clel 2252  df-nfc 2381
  Copyright terms: Public domain W3C validator