Theorem nfeq1 2907

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

Syntax hints:   = wceq 1540  Ⅎwnf 1783  Ⅎwnfc 2876

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 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2721  df-nfc 2878

This theorem is referenced by:  euabsn  4686  invdisjrab  5089  disjxun  5100  iunopeqop  5476  fvelimad  6910  opabiotafun  6923  fvmptt  6970  eusvobj2  7361  oprabv  7429  ovmpodv2  7527  ov3  7532  dom2lem  8940  ttrcltr  9645  pwfseqlem2  10588  fsumf1o  15665  isummulc2  15704  fsum00  15740  isumshft  15781  zprod  15879  fprodf1o  15888  prodss  15889  fprodle  15938  iserodd  16782  yonedalem4b  18213  gsum2d2lem  19879  gsummptnn0fz  19892  gsummoncoe1  22171  elptr2  23437  ovoliunnul  25384  mbfinf  25542  itg2splitlem  25625  dgrle  26124  noinfbnd1  27617  disjabrex  32484  disjabrexf  32485  disjunsn  32496  voliune  34192  volfiniune  34193  bnj958  34903  bnj1491  35020  finminlem  36279  poimirlem23  37610  poimirlem28  37615  cdleme43fsv1snlem  40387  ltrniotaval  40548  cdlemksv2  40814  cdlemkuv2  40834  cdlemk36  40880  cdlemkid  40903  cdlemk19x  40910  eq0rabdioph  42737  monotoddzz  42905  disjinfi  45159  dvnprodlem1  45917  stoweidlem28  45999  stoweidlem48  46019  stoweidlem58  46029  etransclem32  46237  sge0f1o  46353  sge0gtfsumgt  46414  voliunsge0lem  46443