Theorem nfeq2 2909

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

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

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 2701

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 2721  df-nfc 2878

This theorem is referenced by:  eqvincf  3613  csbhypf  3887  nfpr  4652  intab  4938  nfmpt  5200  cbvmptf  5202  cbvmptfg  5203  zfrepclf  5241  eusvnf  5342  reusv2lem4  5351  reusv2  5353  moop2  5457  elrnmpt1  5913  opabiota  6925  fvmptdf  6956  dffo3f  7060  fmptco  7083  elabrex  7198  elabrexg  7199  nfmpo  7451  cbvmpox  7462  ovmpodxf  7519  zfrep6  7913  fmpox  8025  nffrecs  8239  erovlem  8763  xpf1o  9080  mapxpen  9084  wdom2d  9509  cnfcom3clem  9634  scott0  9815  cplem2  9819  infxpenc2lem2  9949  acnlem  9977  fin23lem32  10273  hsmexlem2  10356  axcc3  10367  ac6num  10408  lble  12111  nfsum1  15632  nfsum  15633  zsum  15660  fsum  15662  fsumcvg2  15669  fsum2dlem  15712  infcvgaux1i  15799  nfcprod1  15850  nfcprod  15851  zprod  15879  fprod  15883  fprodser  15891  fprod2dlem  15922  cayleyhamilton1  22812  neiptopreu  23053  xkocnv  23734  istrkg2ld  28440  cnlnadjlem5  32050  chirred  32374  iundisjf  32568  opabdm  32589  opabrn  32590  dfimafnf  32610  fmptcof2  32631  mpomptxf  32651  f1od2  32694  fpwrelmap  32706  elrgspnsubrunlem2  33215  elrspunidl  33392  fedgmullem2  33619  esum2dlem  34075  oms0  34281  bnj1468  34829  bnj981  34933  bnj1463  35038  satfv1  35343  iota5f  35704  nfwlim  35803  bj-seex  36903  isbasisrelowllem1  37336  isbasisrelowllem2  37337  exrecfnlem  37360  finxpreclem6  37377  phpreu  37591  matunitlindflem2  37604  poimirlem24  37631  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  mbfposadd  37654  itg2addnclem  37658  cover2  37702  indexa  37720  riotasvd  38942  cdleme31sn1  40368  cdleme32fva  40424  cdlemk36  40900  elnn0rabdioph  42784  wdom2d2  43017  permaxrep  44989  permaxsep  44990  cbvmpo2  45084  cbvmpo1  45085  elrnmptf  45168  disjrnmpt2  45175  fmuldfeqlem1  45573  climf  45613  climf2  45657  cncficcgt0  45879  stoweidlem8  45999  stoweidlem16  46007  stoweidlem19  46010  stoweidlem21  46012  stoweidlem22  46013  stoweidlem23  46014  stoweidlem29  46020  stoweidlem32  46023  stoweidlem35  46026  stoweidlem36  46027  stoweidlem41  46032  stoweidlem44  46035  stoweidlem45  46036  stoweidlem51  46042  stoweidlem53  46044  stoweidlem60  46051  fourierdlem80  46177  sprsymrelf  47489  cbvmpox2  48317  ovmpordxf  48320  1arymaptfo  48625  2arymaptfo  48636