Theorem nfeq1 2910

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

Syntax hints:   = wceq 1541  Ⅎwnf 1784  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2723  df-nfc 2881

This theorem is referenced by:  euabsn  4674  invdisjrab  5073  disjxun  5084  iunopeqop  5456  fvelimad  6884  opabiotafun  6897  fvmptt  6944  eusvobj2  7333  oprabv  7401  ovmpodv2  7499  ov3  7504  dom2lem  8909  ttrcltr  9601  pwfseqlem2  10545  fsumf1o  15625  isummulc2  15664  fsum00  15700  isumshft  15741  zprod  15839  fprodf1o  15848  prodss  15849  fprodle  15898  iserodd  16742  yonedalem4b  18177  gsum2d2lem  19880  gsummptnn0fz  19893  gsummoncoe1  22218  elptr2  23484  ovoliunnul  25430  mbfinf  25588  itg2splitlem  25671  dgrle  26170  noinfbnd1  27663  disjabrex  32554  disjabrexf  32555  disjunsn  32566  voliune  34234  volfiniune  34235  bnj958  34944  bnj1491  35061  finminlem  36352  poimirlem23  37683  poimirlem28  37688  cdleme43fsv1snlem  40459  ltrniotaval  40620  cdlemksv2  40886  cdlemkuv2  40906  cdlemk36  40952  cdlemkid  40975  cdlemk19x  40982  eq0rabdioph  42809  monotoddzz  42976  disjinfi  45229  dvnprodlem1  45984  stoweidlem28  46066  stoweidlem48  46086  stoweidlem58  46096  etransclem32  46304  sge0f1o  46420  sge0gtfsumgt  46481  voliunsge0lem  46510