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  4572  disjxun  4581  iunopeqop  4906  opabiotafun  6169  fvmptt  6208  eusvobj2  6542  oprabv  6601  ovmpt2dv2  6692  ov3  6695  dom2lem  7881  pwfseqlem2  9360  fsumf1o  14301  isummulc2  14335  fsum00  14371  isumshft  14410  zprod  14506  fprodf1o  14515  prodss  14516  iserodd  15378  yonedalem4b  16739  gsum2d2lem  18195  gsummptnn0fz  18205  gsummoncoe1  19495  elptr2  21187  ovoliunnul  23082  mbfinf  23238  itg2splitlem  23321  dgrle  23803  disjabrex  28777  disjabrexf  28778  disjunsn  28789  voliune  29619  volfiniune  29620  bnj958  30264  bnj1491  30379  finminlem  31482  poimirlem23  32602  poimirlem28  32607  cdleme43fsv1snlem  34726  ltrniotaval  34887  cdlemksv2  35153  cdlemkuv2  35173  cdlemk36  35219  cdlemkid  35242  cdlemk19x  35249  eq0rabdioph  36358  monotoddzz  36526  cncfiooicclem1  38779  stoweidlem28  38921  stoweidlem48  38941  stoweidlem58  38951  etransclem32  39159  sge0gtfsumgt  39336  voliunsge0lem  39365
  Copyright terms: Public domain W3C validator