Theorem nfeq2 2923

Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)

Hypothesis

Ref	Expression
nfeq2.1	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfeq2	⊢ Ⅎ𝑥 𝐴 = 𝐵

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfeq2

Step	Hyp	Ref	Expression
1		nfcv 2906	. 2 ⊢ Ⅎ𝑥𝐴
2		nfeq2.1	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2919	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1539  Ⅎwnf 1787  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-cleq 2730  df-nfc 2888

This theorem is referenced by:  issetf  3436  eqvincf  3572  csbhypf  3857  nfpr  4623  intab  4906  nfmpt  5177  cbvmptf  5179  cbvmptfg  5180  zfrepclf  5213  eusvnf  5310  reusv2lem4  5319  reusv2  5321  moop2  5410  elrnmpt1  5856  opabiota  6833  fvmptdf  6863  fmptco  6983  elabrex  7098  nfmpo  7335  cbvmpox  7346  ovmpodxf  7401  zfrep6  7771  fmpox  7880  nffrecs  8070  nfwrecsOLD  8104  erovlem  8560  xpf1o  8875  mapxpen  8879  wdom2d  9269  cnfcom3clem  9393  scott0  9575  cplem2  9579  infxpenc2lem2  9707  acnlem  9735  fin23lem32  10031  hsmexlem2  10114  axcc3  10125  ac6num  10166  lble  11857  nfsum1  15329  nfsum  15330  nfsumOLD  15331  zsum  15358  fsum  15360  fsumcvg2  15367  fsum2dlem  15410  infcvgaux1i  15497  nfcprod1  15548  nfcprod  15549  zprod  15575  fprod  15579  fprodser  15587  fprod2dlem  15618  cayleyhamilton1  21949  neiptopreu  22192  xkocnv  22873  istrkg2ld  26725  cnlnadjlem5  30334  chirred  30658  iundisjf  30829  opabdm  30852  opabrn  30853  dfimafnf  30872  fmptcof2  30896  mpomptxf  30918  f1od2  30958  fpwrelmap  30970  elrspunidl  31508  fedgmullem2  31613  esum2dlem  31960  oms0  32164  bnj1468  32726  bnj981  32830  bnj1463  32935  satfv1  33225  iota5f  33571  nfwlim  33743  bj-seex  35037  isbasisrelowllem1  35453  isbasisrelowllem2  35454  exrecfnlem  35477  finxpreclem6  35494  phpreu  35688  matunitlindflem2  35701  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  mbfposadd  35751  itg2addnclem  35755  cover2  35799  indexa  35818  riotasvd  36897  cdleme31sn1  38322  cdleme32fva  38378  cdlemk36  38854  elnn0rabdioph  40541  wdom2d2  40773  elabrexg  42478  cbvmpo2  42536  cbvmpo1  42537  dffo3f  42606  elrnmptf  42607  disjrnmpt2  42615  fmuldfeqlem1  43013  climf  43053  climf2  43097  cncficcgt0  43319  stoweidlem8  43439  stoweidlem16  43447  stoweidlem19  43450  stoweidlem21  43452  stoweidlem22  43453  stoweidlem23  43454  stoweidlem29  43460  stoweidlem32  43463  stoweidlem35  43466  stoweidlem36  43467  stoweidlem41  43472  stoweidlem44  43475  stoweidlem45  43476  stoweidlem51  43482  stoweidlem53  43484  stoweidlem60  43491  fourierdlem80  43617  sprsymrelf  44835  cbvmpox2  45559  ovmpordxf  45562  1arymaptfo  45877  2arymaptfo  45888