Theorem nfeq1 2919

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

Syntax hints:   = wceq 1540  Ⅎwnf 1784  Ⅎwnfc 2884

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-ex 1781  df-nf 1785  df-cleq 2728  df-nfc 2886

This theorem is referenced by:  euabsn  4673  invdisjrabw  5074  invdisjrab  5075  disjxun  5087  iunopeqop  5459  fvelimad  6886  opabiotafun  6899  fvmptt  6945  eusvobj2  7322  oprabv  7389  ovmpodv2  7485  ov3  7489  dom2lem  8845  ttrcltr  9565  pwfseqlem2  10508  fsumf1o  15526  isummulc2  15565  fsum00  15601  isumshft  15642  zprod  15738  fprodf1o  15747  prodss  15748  fprodle  15797  iserodd  16625  yonedalem4b  18083  gsum2d2lem  19661  gsummptnn0fz  19674  gsummoncoe1  21573  elptr2  22823  ovoliunnul  24769  mbfinf  24927  itg2splitlem  25011  dgrle  25502  noinfbnd1  26975  disjabrex  31149  disjabrexf  31150  disjunsn  31161  voliune  32436  volfiniune  32437  bnj958  33160  bnj1491  33277  finminlem  34598  poimirlem23  35898  poimirlem28  35903  cdleme43fsv1snlem  38681  ltrniotaval  38842  cdlemksv2  39108  cdlemkuv2  39128  cdlemk36  39174  cdlemkid  39197  cdlemk19x  39204  eq0rabdioph  40848  monotoddzz  41016  disjinfi  43047  stoweidlem28  43894  stoweidlem48  43914  stoweidlem58  43924  etransclem32  44132  sge0gtfsumgt  44307  voliunsge0lem  44336