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  4690  invdisjrab  5094  disjxun  5105  iunopeqop  5481  fvelimad  6928  opabiotafun  6941  fvmptt  6988  eusvobj2  7379  oprabv  7449  ovmpodv2  7547  ov3  7552  dom2lem  8963  ttrcltr  9669  pwfseqlem2  10612  fsumf1o  15689  isummulc2  15728  fsum00  15764  isumshft  15805  zprod  15903  fprodf1o  15912  prodss  15913  fprodle  15962  iserodd  16806  yonedalem4b  18237  gsum2d2lem  19903  gsummptnn0fz  19916  gsummoncoe1  22195  elptr2  23461  ovoliunnul  25408  mbfinf  25566  itg2splitlem  25649  dgrle  26148  noinfbnd1  27641  disjabrex  32511  disjabrexf  32512  disjunsn  32523  voliune  34219  volfiniune  34220  bnj958  34930  bnj1491  35047  finminlem  36306  poimirlem23  37637  poimirlem28  37642  cdleme43fsv1snlem  40414  ltrniotaval  40575  cdlemksv2  40841  cdlemkuv2  40861  cdlemk36  40907  cdlemkid  40930  cdlemk19x  40937  eq0rabdioph  42764  monotoddzz  42932  disjinfi  45186  dvnprodlem1  45944  stoweidlem28  46026  stoweidlem48  46046  stoweidlem58  46056  etransclem32  46264  sge0f1o  46380  sge0gtfsumgt  46441  voliunsge0lem  46470