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

Theorem nfeq1 2970
 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 2955 . 2 𝑥𝐵
31, 2nfeq 2968 1 𝑥 𝐴 = 𝐵
 Colors of variables: wff setvar class Syntax hints:   = wceq 1538  Ⅎwnf 1785  Ⅎwnfc 2936 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-cleq 2791  df-nfc 2938 This theorem is referenced by:  euabsn  4622  invdisjrabw  5015  invdisjrab  5016  disjxun  5028  iunopeqop  5376  fvelimad  6707  opabiotafun  6719  fvmptt  6765  eusvobj2  7128  oprabv  7193  ovmpodv2  7288  ov3  7292  dom2lem  8534  pwfseqlem2  10072  fsumf1o  15074  isummulc2  15111  fsum00  15147  isumshft  15188  zprod  15285  fprodf1o  15294  prodss  15295  fprodle  15344  iserodd  16164  yonedalem4b  17520  gsum2d2lem  19089  gsummptnn0fz  19102  gsummoncoe1  20940  elptr2  22186  ovoliunnul  24118  mbfinf  24276  itg2splitlem  24359  dgrle  24847  disjabrex  30352  disjabrexf  30353  disjunsn  30364  voliune  31610  volfiniune  31611  bnj958  32334  bnj1491  32451  finminlem  33791  poimirlem23  35096  poimirlem28  35101  cdleme43fsv1snlem  37732  ltrniotaval  37893  cdlemksv2  38159  cdlemkuv2  38179  cdlemk36  38225  cdlemkid  38248  cdlemk19x  38255  eq0rabdioph  39732  monotoddzz  39899  disjinfi  41835  stoweidlem28  42685  stoweidlem48  42705  stoweidlem58  42715  etransclem32  42923  sge0gtfsumgt  43097  voliunsge0lem  43126
 Copyright terms: Public domain W3C validator