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

Theorem nfeq 2401
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 2252 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2388 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2388 . . . 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 2381
This theorem is referenced by:  nfel  2402  nfeq1  2403  nfeq2  2405  nfne  2514  raleqf  2707  rexeqf  2708  reueq1f  2709  rmoeq1f  2710  rabeqf  2756  sbceqg  3072  csbhypf  3091  nffn  5278  nffo  5388  fvmptdf  5545  mpteqb  5548  fvmptf  5550  eqfnfv2f  5560  dff13f  5718  ovmpt2s  5905  ov2gf  5906  ovmpt2dxf  5907  ovmpt2df  5913  opabiota  6259  eqerlem  6660  sumeq1f  12127  sumeq2w  12131  sumeq2ii  12132  sumss  12163  fsumadd  12177  fsummulc2  12212  fsumrelem  12231  txcnp  17277  ptcnplem  17278  cnmpt11  17320  cnmpt21  17328  cnmptcom  17335  mbfeqalem  18960  mbflim  18986  itgeq1f  19089  itgeqa  19131  dvmptfsum  19285  ulmss  19737  leibpi  20201  o1cxp  20232  lgseisenlem2  20552  dfimafnf  23003  prodeq3ii  24676  fprodadd  24720  fprodneg  24746  fprodsub  24747  subtr  25592  subtr2  25593  dvdsrabdioph  26259  fphpd  26267  fvelrnbf  27058  refsum2cnlem1  27077  fmuldfeqlem1  27081  fmuldfeq  27082  climmulf  27099  climexp  27100  climsuse  27103  climrecf  27104  stoweidlem8  27126  stoweidlem16  27134  stoweidlem18  27136  stoweidlem19  27137  stoweidlem21  27139  stoweidlem22  27140  stoweidlem23  27141  stoweidlem28  27146  stoweidlem29  27147  stoweidlem31  27149  stoweidlem32  27150  stoweidlem35  27153  stoweidlem36  27154  stoweidlem41  27159  stoweidlem44  27162  stoweidlem45  27163  stoweidlem48  27166  stoweidlem51  27169  stoweidlem53  27171  stoweidlem55  27173  stoweidlem58  27176  stoweidlem59  27177  stoweidlem60  27178  bnj1316  27985  bnj1446  28207  bnj1447  28208  bnj1448  28209  bnj1519  28227  bnj1520  28228  bnj1529  28232
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 2239
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 2251  df-clel 2254  df-nfc 2383
  Copyright terms: Public domain W3C validator