Theorem nfeq1 2908

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

Syntax hints:   = wceq 1540  Ⅎwnf 1783  Ⅎwnfc 2877

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2722  df-nfc 2879

This theorem is referenced by:  euabsn  4693  invdisjrab  5097  disjxun  5108  iunopeqop  5484  fvelimad  6931  opabiotafun  6944  fvmptt  6991  eusvobj2  7382  oprabv  7452  ovmpodv2  7550  ov3  7555  dom2lem  8966  ttrcltr  9676  pwfseqlem2  10619  fsumf1o  15696  isummulc2  15735  fsum00  15771  isumshft  15812  zprod  15910  fprodf1o  15919  prodss  15920  fprodle  15969  iserodd  16813  yonedalem4b  18244  gsum2d2lem  19910  gsummptnn0fz  19923  gsummoncoe1  22202  elptr2  23468  ovoliunnul  25415  mbfinf  25573  itg2splitlem  25656  dgrle  26155  noinfbnd1  27648  disjabrex  32518  disjabrexf  32519  disjunsn  32530  voliune  34226  volfiniune  34227  bnj958  34937  bnj1491  35054  finminlem  36313  poimirlem23  37644  poimirlem28  37649  cdleme43fsv1snlem  40421  ltrniotaval  40582  cdlemksv2  40848  cdlemkuv2  40868  cdlemk36  40914  cdlemkid  40937  cdlemk19x  40944  eq0rabdioph  42771  monotoddzz  42939  disjinfi  45193  dvnprodlem1  45951  stoweidlem28  46033  stoweidlem48  46053  stoweidlem58  46063  etransclem32  46271  sge0f1o  46387  sge0gtfsumgt  46448  voliunsge0lem  46477