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

Theorem nfeq 2439
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 2290 . 2  |-  ( A  =  B  <->  A. z
( z  e.  A  <->  z  e.  B ) )
2 nfnfc.1 . . . . 5  |-  F/_ x A
32nfcri 2426 . . . 4  |-  F/ x  z  e.  A
4 nfeq.2 . . . . 5  |-  F/_ x B
54nfcri 2426 . . . 4  |-  F/ x  z  e.  B
63, 5nfbi 1784 . . 3  |-  F/ x
( z  e.  A  <->  z  e.  B )
76nfal 1778 . 2  |-  F/ x A. z ( z  e.  A  <->  z  e.  B
)
81, 7nfxfr 1560 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1530   F/wnf 1534    = wceq 1632    e. wcel 1696   F/_wnfc 2419
This theorem is referenced by:  nfel  2440  nfeq1  2441  nfeq2  2443  nfne  2552  raleqf  2745  rexeqf  2746  reueq1f  2747  rmoeq1f  2748  rabeqf  2794  sbceqg  3110  csbhypf  3129  nffn  5356  nffo  5466  fvmptdf  5627  mpteqb  5630  fvmptf  5632  eqfnfv2f  5642  dff13f  5800  ovmpt2s  5987  ov2gf  5988  ovmpt2dxf  5989  ovmpt2df  5995  opabiota  6309  eqerlem  6708  sumeq1f  12177  sumeq2w  12181  sumeq2ii  12182  sumss  12213  fsumadd  12227  fsummulc2  12262  fsumrelem  12281  txcnp  17330  ptcnplem  17331  cnmpt11  17373  cnmpt21  17381  cnmptcom  17388  mbfeqalem  19013  mbflim  19039  itgeq1f  19142  itgeqa  19184  dvmptfsum  19338  ulmss  19790  leibpi  20254  o1cxp  20285  lgseisenlem2  20605  dfimafnf  23057  disjabrex  23374  disjabrexf  23375  iundisjf  23380  cprodeq1f  24130  cprodeq2w  24134  cprodeq2ii  24135  prodeq3ii  25411  fprodadd  25455  fprodneg  25481  fprodsub  25482  subtr  26327  subtr2  26328  dvdsrabdioph  26994  fphpd  27002  fvelrnbf  27792  refsum2cnlem1  27811  fmuldfeqlem1  27815  fmuldfeq  27816  climmulf  27833  climexp  27834  climsuse  27837  climrecf  27838  stoweidlem8  27860  stoweidlem16  27868  stoweidlem18  27870  stoweidlem19  27871  stoweidlem21  27873  stoweidlem22  27874  stoweidlem23  27875  stoweidlem28  27880  stoweidlem29  27881  stoweidlem31  27883  stoweidlem32  27884  stoweidlem35  27887  stoweidlem36  27888  stoweidlem41  27893  stoweidlem44  27896  stoweidlem45  27897  stoweidlem48  27900  stoweidlem51  27903  stoweidlem53  27905  stoweidlem55  27907  stoweidlem58  27910  stoweidlem59  27911  stoweidlem60  27912  bnj1316  29169  bnj1446  29391  bnj1447  29392  bnj1448  29393  bnj1519  29411  bnj1520  29412  bnj1529  29416
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421
  Copyright terms: Public domain W3C validator