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

Step	Hyp	Ref	Expression
1		nfeq1.1	. 2 ⊢ Ⅎ𝑥𝐴
2		nfcv 2905	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2919	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

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