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

Theorem nfeq1 2580
Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq1.1  |-  F/_ x A
Assertion
Ref Expression
nfeq1  |-  F/ x  A  =  B
Distinct variable group:    x, B
Allowed substitution hint:    A( x)

Proof of Theorem nfeq1
StepHypRef Expression
1 nfeq1.1 . 2  |-  F/_ x A
2 nfcv 2571 . 2  |-  F/_ x B
31, 2nfeq 2578 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1553    = wceq 1652   F/_wnfc 2558
This theorem is referenced by:  euabsn  3868  disjxun  4202  reusv6OLD  4726  fvmptt  5812  ovmpt2dv2  6199  ov3  6202  opabiotafun  6528  eusvobj2  6574  dom2lem  7139  pwfseqlem2  8526  zsum  12504  fsumf1o  12509  isummulc2  12538  fsum00  12569  isumshft  12611  iserodd  13201  yonedalem4b  14365  gsum2d2lem  15539  elptr2  17598  ovoliunnul  19395  mbfinf  19549  itg2splitlem  19632  dgrle  20154  disjabrex  24016  disjabrexf  24017  voliune  24577  volfiniune  24578  zprod  25255  fprodf1o  25264  prodss  25265  finminlem  26302  eq0rabdioph  26816  monotoddzz  26987  stoweidlem28  27734  stoweidlem48  27754  stoweidlem58  27764  bnj958  29238  bnj1491  29353  cdleme43fsv1snlem  31144  ltrniotaval  31305  cdlemksv2  31571  cdlemkuv2  31591  cdlemk36  31637  cdlemkid  31660  cdlemk19x  31667
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