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

Theorem nfeq1 2921
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 2905 . 2 𝑥𝐵
31, 2nfeq 2919 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wnf 1783  wnfc 2890
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2729  df-nfc 2892
This theorem is referenced by:  euabsn  4726  invdisjrab  5130  disjxun  5141  iunopeqop  5526  fvelimad  6976  opabiotafun  6989  fvmptt  7036  eusvobj2  7423  oprabv  7493  ovmpodv2  7591  ov3  7596  dom2lem  9032  ttrcltr  9756  pwfseqlem2  10699  fsumf1o  15759  isummulc2  15798  fsum00  15834  isumshft  15875  zprod  15973  fprodf1o  15982  prodss  15983  fprodle  16032  iserodd  16873  yonedalem4b  18321  gsum2d2lem  19991  gsummptnn0fz  20004  gsummoncoe1  22312  elptr2  23582  ovoliunnul  25542  mbfinf  25700  itg2splitlem  25783  dgrle  26282  noinfbnd1  27774  disjabrex  32595  disjabrexf  32596  disjunsn  32607  voliune  34230  volfiniune  34231  bnj958  34954  bnj1491  35071  finminlem  36319  poimirlem23  37650  poimirlem28  37655  cdleme43fsv1snlem  40422  ltrniotaval  40583  cdlemksv2  40849  cdlemkuv2  40869  cdlemk36  40915  cdlemkid  40938  cdlemk19x  40945  eq0rabdioph  42787  monotoddzz  42955  disjinfi  45197  dvnprodlem1  45961  stoweidlem28  46043  stoweidlem48  46063  stoweidlem58  46073  etransclem32  46281  sge0f1o  46397  sge0gtfsumgt  46458  voliunsge0lem  46487
  Copyright terms: Public domain W3C validator