Theorem nfeq1 2916

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

Syntax hints:   = wceq 1547  Ⅎwnf 1790  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-cleq 2731  df-nfc 2888

This theorem is referenced by:  euabsn  4658  invdisjrab  5059  disjxun  5070  iunopeqop  5462  iunopeqopOLD  5463  fvelimad  6894  opabiotafun  6907  fvmptt  6956  eusvobj2  7348  oprabv  7416  ovmpodv2  7514  ov3  7519  dom2lem  8929  ttrcltr  9628  pwfseqlem2  10573  fsumf1o  15676  isummulc2  15715  fsum00  15752  isumshft  15795  zprod  15893  fprodf1o  15902  prodss  15903  fprodle  15952  iserodd  16797  yonedalem4b  18233  gsum2d2lem  19939  gsummptnn0fz  19952  gsummoncoe1  22294  elptr2  23557  ovoliunnul  25492  mbfinf  25650  itg2splitlem  25733  dgrle  26226  noinfbnd1  27711  disjabrex  32671  disjabrexf  32672  disjunsn  32683  voliune  34413  volfiniune  34414  bnj958  35122  bnj1491  35239  finminlem  36546  poimirlem23  38010  poimirlem28  38015  cdleme43fsv1snlem  40912  ltrniotaval  41073  cdlemksv2  41339  cdlemkuv2  41359  cdlemk36  41405  cdlemkid  41428  cdlemk19x  41435  eq0rabdioph  43225  monotoddzz  43388  disjinfi  45639  dvnprodlem1  46389  stoweidlem28  46471  stoweidlem48  46491  stoweidlem58  46501  etransclem32  46709  sge0f1o  46825  sge0gtfsumgt  46886  voliunsge0lem  46915