Theorem nfeq2 2910

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

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

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 2702

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 2722  df-nfc 2879

This theorem is referenced by:  eqvincf  3619  csbhypf  3893  nfpr  4659  intab  4945  nfmpt  5208  cbvmptf  5210  cbvmptfg  5211  zfrepclf  5249  eusvnf  5350  reusv2lem4  5359  reusv2  5361  moop2  5465  elrnmpt1  5927  opabiota  6946  fvmptdf  6977  dffo3f  7081  fmptco  7104  elabrex  7219  elabrexg  7220  nfmpo  7474  cbvmpox  7485  ovmpodxf  7542  zfrep6  7936  fmpox  8049  nffrecs  8265  erovlem  8789  xpf1o  9109  mapxpen  9113  wdom2d  9540  cnfcom3clem  9665  scott0  9846  cplem2  9850  infxpenc2lem2  9980  acnlem  10008  fin23lem32  10304  hsmexlem2  10387  axcc3  10398  ac6num  10439  lble  12142  nfsum1  15663  nfsum  15664  zsum  15691  fsum  15693  fsumcvg2  15700  fsum2dlem  15743  infcvgaux1i  15830  nfcprod1  15881  nfcprod  15882  zprod  15910  fprod  15914  fprodser  15922  fprod2dlem  15953  cayleyhamilton1  22786  neiptopreu  23027  xkocnv  23708  istrkg2ld  28394  cnlnadjlem5  32007  chirred  32331  iundisjf  32525  opabdm  32546  opabrn  32547  dfimafnf  32567  fmptcof2  32588  mpomptxf  32608  f1od2  32651  fpwrelmap  32663  elrgspnsubrunlem2  33206  elrspunidl  33406  fedgmullem2  33633  esum2dlem  34089  oms0  34295  bnj1468  34843  bnj981  34947  bnj1463  35052  satfv1  35357  iota5f  35718  nfwlim  35817  bj-seex  36917  isbasisrelowllem1  37350  isbasisrelowllem2  37351  exrecfnlem  37374  finxpreclem6  37391  phpreu  37605  matunitlindflem2  37618  poimirlem24  37645  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  mbfposadd  37668  itg2addnclem  37672  cover2  37716  indexa  37734  riotasvd  38956  cdleme31sn1  40382  cdleme32fva  40438  cdlemk36  40914  elnn0rabdioph  42798  wdom2d2  43031  permaxrep  45003  permaxsep  45004  cbvmpo2  45098  cbvmpo1  45099  elrnmptf  45182  disjrnmpt2  45189  fmuldfeqlem1  45587  climf  45627  climf2  45671  cncficcgt0  45893  stoweidlem8  46013  stoweidlem16  46021  stoweidlem19  46024  stoweidlem21  46026  stoweidlem22  46027  stoweidlem23  46028  stoweidlem29  46034  stoweidlem32  46037  stoweidlem35  46040  stoweidlem36  46041  stoweidlem41  46046  stoweidlem44  46049  stoweidlem45  46050  stoweidlem51  46056  stoweidlem53  46058  stoweidlem60  46065  fourierdlem80  46191  sprsymrelf  47500  cbvmpox2  48328  ovmpordxf  48331  1arymaptfo  48636  2arymaptfo  48647