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 1533  Ⅎwnf 1777  Ⅎwnfc 2875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778  df-cleq 2717  df-nfc 2877

This theorem is referenced by:  euabsn  4732  invdisjrabw  5134  invdisjrab  5135  disjxun  5147  iunopeqop  5523  fvelimad  6965  opabiotafun  6978  fvmptt  7024  eusvobj2  7411  oprabv  7480  ovmpodv2  7579  ov3  7584  dom2lem  9013  ttrcltr  9741  pwfseqlem2  10684  fsumf1o  15705  isummulc2  15744  fsum00  15780  isumshft  15821  zprod  15917  fprodf1o  15926  prodss  15927  fprodle  15976  iserodd  16807  yonedalem4b  18271  gsum2d2lem  19940  gsummptnn0fz  19953  gsummoncoe1  22252  elptr2  23522  ovoliunnul  25480  mbfinf  25638  itg2splitlem  25722  dgrle  26222  noinfbnd1  27708  disjabrex  32451  disjabrexf  32452  disjunsn  32463  voliune  33979  volfiniune  33980  bnj958  34702  bnj1491  34819  finminlem  35933  poimirlem23  37247  poimirlem28  37252  cdleme43fsv1snlem  40023  ltrniotaval  40184  cdlemksv2  40450  cdlemkuv2  40470  cdlemk36  40516  cdlemkid  40539  cdlemk19x  40546  eq0rabdioph  42338  monotoddzz  42506  disjinfi  44704  stoweidlem28  45554  stoweidlem48  45574  stoweidlem58  45584  etransclem32  45792  sge0gtfsumgt  45969  voliunsge0lem  45998