Theorem nfeq1 2946

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

Syntax hints:   = wceq 1567  Ⅎwnf 1810  Ⅎwnfc 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-cleq 2761  df-nfc 2918

This theorem is referenced by:  euabsn  4694  invdisjrab  5097  disjxun  5108  iunopeqop  5502  iunopeqopOLD  5503  fvelimad  6946  opabiotafun  6959  fvmptt  7008  eusvobj2  7400  oprabv  7468  ovmpodv2  7566  ov3  7571  dom2lem  8985  ttrcltr  9681  pwfseqlem2  10640  fsumf1o  15770  isummulc2  15809  fsum00  15846  isumshft  15889  zprod  15987  fprodf1o  15996  prodss  15997  fprodle  16046  iserodd  16891  yonedalem4b  18328  gsum2d2lem  20039  gsummptnn0fz  20052  gsummoncoe1  22433  elptr2  23696  ovoliunnul  25631  mbfinf  25789  itg2splitlem  25872  dgrle  26365  noinfbnd1  27855  disjabrex  32864  disjabrexf  32865  disjunsn  32876  voliune  34560  volfiniune  34561  bnj958  35269  bnj1491  35386  finminlem  36714  poimirlem23  38177  poimirlem28  38182  cdleme43fsv1snlem  41079  ltrniotaval  41240  cdlemksv2  41506  cdlemkuv2  41526  cdlemk36  41572  cdlemkid  41595  cdlemk19x  41602  eq0rabdioph  43392  monotoddzz  43555  disjinfi  45795  dvnprodlem1  46545  stoweidlem28  46627  stoweidlem48  46647  stoweidlem58  46657  etransclem32  46865  sge0f1o  46981  sge0gtfsumgt  47042  voliunsge0lem  47071  sssmf  47337