Theorem nfeq1 2911

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

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

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 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

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 2725  df-nfc 2882

This theorem is referenced by:  euabsn  4680  invdisjrab  5082  disjxun  5093  iunopeqop  5466  fvelimad  6898  opabiotafun  6911  fvmptt  6958  eusvobj2  7347  oprabv  7415  ovmpodv2  7513  ov3  7518  dom2lem  8925  ttrcltr  9617  pwfseqlem2  10561  fsumf1o  15637  isummulc2  15676  fsum00  15712  isumshft  15753  zprod  15851  fprodf1o  15860  prodss  15861  fprodle  15910  iserodd  16754  yonedalem4b  18190  gsum2d2lem  19893  gsummptnn0fz  19906  gsummoncoe1  22243  elptr2  23509  ovoliunnul  25455  mbfinf  25613  itg2splitlem  25696  dgrle  26195  noinfbnd1  27688  disjabrex  32583  disjabrexf  32584  disjunsn  32595  voliune  34314  volfiniune  34315  bnj958  35024  bnj1491  35141  finminlem  36434  poimirlem23  37756  poimirlem28  37761  cdleme43fsv1snlem  40592  ltrniotaval  40753  cdlemksv2  41019  cdlemkuv2  41039  cdlemk36  41085  cdlemkid  41108  cdlemk19x  41115  eq0rabdioph  42933  monotoddzz  43100  disjinfi  45352  dvnprodlem1  46106  stoweidlem28  46188  stoweidlem48  46208  stoweidlem58  46218  etransclem32  46426  sge0f1o  46542  sge0gtfsumgt  46603  voliunsge0lem  46632