Theorem nfeq1 2778

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

Syntax hints:   = wceq 1483  Ⅎwnf 1708  Ⅎwnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-nfc 2753

This theorem is referenced by:  euabsn  4261  invdisjrab  4639  disjxun  4651  iunopeqop  4981  opabiotafun  6259  fvmptt  6300  eusvobj2  6643  oprabv  6703  ovmpt2dv2  6794  ov3  6797  dom2lem  7995  pwfseqlem2  9481  fsumf1o  14454  isummulc2  14493  fsum00  14530  isumshft  14571  zprod  14667  fprodf1o  14676  prodss  14677  iserodd  15540  yonedalem4b  16916  gsum2d2lem  18372  gsummptnn0fz  18382  gsummoncoe1  19674  elptr2  21377  ovoliunnul  23275  mbfinf  23432  itg2splitlem  23515  dgrle  23999  disjabrex  29395  disjabrexf  29396  disjunsn  29407  voliune  30292  volfiniune  30293  bnj958  31010  bnj1491  31125  finminlem  32312  poimirlem23  33432  poimirlem28  33437  cdleme43fsv1snlem  35708  ltrniotaval  35869  cdlemksv2  36135  cdlemkuv2  36155  cdlemk36  36201  cdlemkid  36224  cdlemk19x  36231  eq0rabdioph  37340  monotoddzz  37508  cncfiooicclem1  40106  stoweidlem28  40245  stoweidlem48  40265  stoweidlem58  40275  etransclem32  40483  sge0gtfsumgt  40660  voliunsge0lem  40689