Theorem nfeq1 2940

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 2925	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2938	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1570  Ⅎwnf 1813  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-cleq 2755  df-nfc 2912

This theorem is referenced by:  euabsn  4693  invdisjrab  5097  disjxun  5108  iunopeqop  5506  iunopeqopOLD  5507  fvelimad  6950  opabiotafun  6963  fvmptt  7012  eusvobj2  7404  oprabv  7472  ovmpodv2  7570  ov3  7575  dom2lem  8990  ttrcltr  9686  pwfseqlem2  10645  fsumf1o  15776  isummulc2  15815  fsum00  15852  isumshft  15895  zprod  15993  fprodf1o  16002  prodss  16003  fprodle  16052  iserodd  16896  yonedalem4b  18333  gsum2d2lem  20044  gsummptnn0fz  20057  gsummoncoe1  22449  elptr2  23712  ovoliunnul  25647  mbfinf  25805  itg2splitlem  25888  dgrle  26381  noinfbnd1  27874  disjabrex  32908  disjabrexf  32909  disjunsn  32920  voliune  34600  volfiniune  34601  bnj958  35309  bnj1491  35426  finminlem  36810  poimirlem23  38275  poimirlem28  38280  cdleme43fsv1snlem  41175  ltrniotaval  41336  cdlemksv2  41602  cdlemkuv2  41622  cdlemk36  41668  cdlemkid  41691  cdlemk19x  41698  eq0rabdioph  43490  monotoddzz  43653  disjinfi  45893  dvnprodlem1  46643  stoweidlem28  46725  stoweidlem48  46745  stoweidlem58  46755  etransclem32  46963  sge0f1o  47079  sge0gtfsumgt  47140  voliunsge0lem  47169  sssmf  47435