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 1570  Ⅎwnf 1816  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-cleq 2752  df-nfc 2909

This theorem is used by:  euabsn  4687  invdisjrab  5090  disjxun  5101  iunopeqop  5498  iunopeqopOLD  5499  fvelimad  6945  opabiotafun  6958  fvmptt  7007  eusvobj2  7405  oprabv  7473  ovmpodv2  7571  ov3  7576  dom2lem  8998  ttrcltr  9695  pwfseqlem2  10668  fsumf1o  15809  isummulc2  15848  fsum00  15885  isumshft  15928  zprod  16024  fprodf1o  16033  prodss  16034  fprodle  16083  iserodd  16927  yonedalem4b  18364  gsum2d2lem  20100  gsummptnn0fz  20113  gsummoncoe1  22533  elptr2  23800  ovoliunnul  25735  mbfinf  25893  itg2splitlem  25976  dgrle  26469  noinfbnd1  27965  disjabrex  33055  disjabrexf  33056  disjunsn  33067  voliune  34740  volfiniune  34741  bnj958  35449  bnj1491  35566  finminlem  36937  poimirlem23  38392  poimirlem28  38397  cdleme43fsv1snlem  41293  ltrniotaval  41454  cdlemksv2  41720  cdlemkuv2  41740  cdlemk36  41786  cdlemkid  41809  cdlemk19x  41816  eq0rabdioph  43621  monotoddzz  43784  disjinfi  46024  dvnprodlem1  46774  stoweidlem28  46856  stoweidlem48  46876  stoweidlem58  46886  etransclem32  47094  sge0f1o  47210  sge0gtfsumgt  47271  voliunsge0lem  47300  sssmf  47566