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

Theorem nfeq1 2990
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 2974 . 2 𝑥𝐵
31, 2nfeq 2988 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wnf 1775  wnfc 2958
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-cleq 2811  df-nfc 2960
This theorem is referenced by:  euabsn  4654  invdisjrabw  5042  invdisjrab  5043  disjxun  5055  iunopeqop  5402  fvelimad  6725  opabiotafun  6737  fvmptt  6780  eusvobj2  7138  oprabv  7203  ovmpodv2  7297  ov3  7300  dom2lem  8537  pwfseqlem2  10069  fsumf1o  15068  isummulc2  15105  fsum00  15141  isumshft  15182  zprod  15279  fprodf1o  15288  prodss  15289  fprodle  15338  iserodd  16160  yonedalem4b  17514  gsum2d2lem  19022  gsummptnn0fz  19035  gsummoncoe1  20400  elptr2  22110  ovoliunnul  24035  mbfinf  24193  itg2splitlem  24276  dgrle  24760  disjabrex  30260  disjabrexf  30261  disjunsn  30272  voliune  31387  volfiniune  31388  bnj958  32111  bnj1491  32226  finminlem  33563  poimirlem23  34796  poimirlem28  34801  cdleme43fsv1snlem  37436  ltrniotaval  37597  cdlemksv2  37863  cdlemkuv2  37883  cdlemk36  37929  cdlemkid  37952  cdlemk19x  37959  eq0rabdioph  39251  monotoddzz  39418  stoweidlem28  42190  stoweidlem48  42210  stoweidlem58  42220  etransclem32  42428  sge0gtfsumgt  42602  voliunsge0lem  42631
  Copyright terms: Public domain W3C validator