Theorem nfeq1 2961

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

Syntax hints:   = wceq 1522  Ⅎwnf 1766  Ⅎwnfc 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1763  df-nf 1767  df-cleq 2787  df-nfc 2934

This theorem is referenced by:  euabsn  4571  invdisjrab  4951  disjxun  4962  iunopeqop  5305  fvelimad  6603  opabiotafun  6614  fvmptt  6657  eusvobj2  7012  oprabv  7076  ovmpodv2  7167  ov3  7170  dom2lem  8400  pwfseqlem2  9930  fsumf1o  14913  isummulc2  14950  fsum00  14986  isumshft  15027  zprod  15124  fprodf1o  15133  prodss  15134  fprodle  15183  iserodd  16001  yonedalem4b  17355  gsum2d2lem  18813  gsummptnn0fz  18823  gsummoncoe1  20155  elptr2  21866  ovoliunnul  23791  mbfinf  23949  itg2splitlem  24032  dgrle  24516  disjabrex  30014  disjabrexf  30015  disjunsn  30026  voliune  31097  volfiniune  31098  bnj958  31820  bnj1491  31935  finminlem  33269  poimirlem23  34459  poimirlem28  34464  cdleme43fsv1snlem  37100  ltrniotaval  37261  cdlemksv2  37527  cdlemkuv2  37547  cdlemk36  37593  cdlemkid  37616  cdlemk19x  37623  eq0rabdioph  38871  monotoddzz  39038  stoweidlem28  41869  stoweidlem48  41889  stoweidlem58  41899  etransclem32  42107  sge0gtfsumgt  42281  voliunsge0lem  42310