Theorem nfeq1 2924

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

Syntax hints:   = wceq 1537  Ⅎwnf 1781  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-cleq 2732  df-nfc 2895

This theorem is referenced by:  euabsn  4751  invdisjrab  5153  disjxun  5164  iunopeqop  5540  fvelimad  6989  opabiotafun  7002  fvmptt  7049  eusvobj2  7440  oprabv  7510  ovmpodv2  7608  ov3  7613  dom2lem  9052  ttrcltr  9785  pwfseqlem2  10728  fsumf1o  15771  isummulc2  15810  fsum00  15846  isumshft  15887  zprod  15985  fprodf1o  15994  prodss  15995  fprodle  16044  iserodd  16882  yonedalem4b  18346  gsum2d2lem  20015  gsummptnn0fz  20028  gsummoncoe1  22333  elptr2  23603  ovoliunnul  25561  mbfinf  25719  itg2splitlem  25803  dgrle  26302  noinfbnd1  27792  disjabrex  32604  disjabrexf  32605  disjunsn  32616  voliune  34193  volfiniune  34194  bnj958  34916  bnj1491  35033  finminlem  36284  poimirlem23  37603  poimirlem28  37608  cdleme43fsv1snlem  40377  ltrniotaval  40538  cdlemksv2  40804  cdlemkuv2  40824  cdlemk36  40870  cdlemkid  40893  cdlemk19x  40900  eq0rabdioph  42732  monotoddzz  42900  disjinfi  45099  stoweidlem28  45949  stoweidlem48  45969  stoweidlem58  45979  etransclem32  46187  sge0gtfsumgt  46364  voliunsge0lem  46393