Theorem nfeq2 2941

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

Syntax hints:   = wceq 1560  Ⅎwnf 1803  Ⅎwnfc 2909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804  df-cleq 2754  df-nfc 2911

This theorem is referenced by:  eqvincf  3609  csbhypf  3880  nfpr  4651  intab  4936  nfmpt  5198  cbvmptf  5200  cbvmptfg  5201  zfrepclf  5241  eusvnf  5349  reusv2lem4  5358  reusv2  5360  moop2  5471  elrnmpt1  5936  opabiota  6949  fvmptdf  6982  dffo3f  7087  fmptco  7111  elabrex  7226  elabrexg  7227  nfmpo  7478  cbvmpox  7489  ovmpodxf  7546  zfrep6OLD  7936  fmpox  8048  nffrecs  8264  erovlem  8795  xpf1o  9111  mapxpen  9115  wdom2d  9528  cnfcom3clem  9660  scott0  9844  cplem2  9848  infxpenc2lem2  9976  acnlem  10004  fin23lem32  10301  hsmexlem2  10384  axcc3  10395  ac6num  10436  lble  12144  nfsum1  15717  nfsum  15718  zsum  15745  fsum  15747  fsumcvg2  15754  fsum2dlem  15797  infcvgaux1i  15887  nfcprod1  15938  nfcprod  15939  zprod  15967  fprod  15971  fprodser  15979  fprod2dlem  16010  cayleyhamilton1  22949  neiptopreu  23190  xkocnv  23871  istrkg2ld  28626  cnlnadjlem5  32271  chirred  32595  iundisjf  32786  opabdm  32810  opabrn  32811  dfimafnf  32835  fmptcof2  32856  mpomptxf  32877  f1od2  32918  fpwrelmap  32932  elrgspnsubrunlem2  33426  elrspunidl  33611  mplvrpmga  33839  esplyfval1  33867  fedgmullem2  33924  esum2dlem  34386  oms0  34591  bnj1468  35138  bnj981  35242  bnj1463  35347  satfv1  35710  iota5f  36071  nfwlim  36167  bj-seex  37404  isbasisrelowllem1  37846  isbasisrelowllem2  37847  exrecfnlem  37870  finxpreclem6  37887  phpreu  38100  matunitlindflem2  38113  poimirlem24  38140  poimirlem25  38141  poimirlem26  38142  poimirlem27  38143  mbfposadd  38163  itg2addnclem  38167  cover2  38211  indexa  38229  riotasvd  39577  cdleme31sn1  41002  cdleme32fva  41058  cdlemk36  41534  elnn0rabdioph  43377  wdom2d2  43609  permaxrep  45579  permaxsep  45580  cbvmpo2  45672  cbvmpo1  45673  elrnmptf  45756  disjrnmpt2  45763  fmuldfeqlem1  46155  climf  46195  climf2  46237  cncficcgt0  46459  stoweidlem8  46579  stoweidlem16  46587  stoweidlem19  46590  stoweidlem21  46592  stoweidlem22  46593  stoweidlem23  46594  stoweidlem29  46600  stoweidlem32  46603  stoweidlem35  46606  stoweidlem36  46607  stoweidlem41  46612  stoweidlem44  46615  stoweidlem45  46616  stoweidlem51  46622  stoweidlem53  46624  stoweidlem60  46631  fourierdlem80  46757  sprsymrelf  48098  cbvmpox2  48955  ovmpordxf  48958  1arymaptfo  49262  2arymaptfo  49273