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

Theorem nfeq1 2764
Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq1.1 𝑥𝐴
Assertion
Ref Expression
nfeq1 𝑥 𝐴 = 𝐵
Distinct variable group:   𝑥,𝐵
Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem nfeq1
StepHypRef Expression
1 nfeq1.1 . 2 𝑥𝐴
2 nfcv 2751 . 2 𝑥𝐵
31, 2nfeq 2762 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  wnf 1699  wnfc 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-nfc 2740
This theorem is referenced by:  euabsn  4205  invdisjrab  4567  disjxun  4576  opabiotafun  6154  fvmptt  6193  eusvobj2  6520  oprabv  6579  ovmpt2dv2  6670  ov3  6673  dom2lem  7859  pwfseqlem2  9338  fsumf1o  14250  isummulc2  14284  fsum00  14320  isumshft  14359  zprod  14455  fprodf1o  14464  prodss  14465  iserodd  15327  yonedalem4b  16688  gsum2d2lem  18144  gsummptnn0fz  18154  gsummoncoe1  19444  elptr2  21135  ovoliunnul  23027  mbfinf  23183  itg2splitlem  23266  dgrle  23748  disjabrex  28571  disjabrexf  28572  disjunsn  28583  voliune  29413  volfiniune  29414  bnj958  30058  bnj1491  30173  finminlem  31276  poimirlem23  32396  poimirlem28  32401  cdleme43fsv1snlem  34520  ltrniotaval  34681  cdlemksv2  34947  cdlemkuv2  34967  cdlemk36  35013  cdlemkid  35036  cdlemk19x  35043  eq0rabdioph  36152  monotoddzz  36320  cncfiooicclem1  38573  stoweidlem28  38715  stoweidlem48  38735  stoweidlem58  38745  etransclem32  38953  sge0gtfsumgt  39130  voliunsge0lem  39159  iunopeqop  40121
  Copyright terms: Public domain W3C validator