Theorem nfeq1 2937

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

This proof depends on syntax axioms:   = wceq 1569  Ⅎwnf 1815  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-cleq 2752  df-nfc 2909

This theorem is used by:  euabsn  4683  invdisjrab  5089  disjxun  5100  iunopeqop  5493  iunopeqopOLD  5494  fvelimad  6953  opabiotafun  6966  fvmptt  7015  eusvobj2  7413  oprabv  7481  ovmpodv2  7579  ov3  7584  dom2lem  9023  ttrcltr  9721  pwfseqlem2  10748  fsumf1o  15895  isummulc2  15934  fsum00  15971  isumshft  16014  zprod  16110  fprodf1o  16119  prodss  16120  fprodle  16169  iserodd  17019  yonedalem4b  18456  gsum2d2lem  20193  gsummptnn0fz  20206  gsummoncoe1  22632  elptr2  23899  ovoliunnul  25834  mbfinf  25992  itg2splitlem  26075  dgrle  26568  noinfbnd1  28092  disjabrex  33224  disjabrexf  33225  disjunsn  33236  voliune  34909  volfiniune  34910  bnj958  35617  bnj1491  35734  srepdflem1  36005  finminlem  37199  poimirlem23  38655  poimirlem28  38660  cdleme43fsv1snlem  41571  ltrniotaval  41732  cdlemksv2  41998  cdlemkuv2  42018  cdlemk36  42064  cdlemkid  42087  cdlemk19x  42094  eq0rabdioph  43881  monotoddzz  44044  disjinfi  46301  dvnprodlem1  47050  stoweidlem28  47132  stoweidlem48  47152  stoweidlem58  47162  etransclem32  47370  sge0f1o  47486  sge0gtfsumgt  47547  voliunsge0lem  47576  sssmf  47842