Theorem nfeq2 2995

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

Syntax hints:   = wceq 1537  Ⅎwnf 1784  Ⅎwnfc 2961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-cleq 2814  df-nfc 2963

This theorem is referenced by:  issetf  3507  eqvincf  3643  csbhypf  3911  nfpr  4628  intab  4906  nfmpt  5163  cbvmptf  5165  cbvmptfg  5166  zfrepclf  5198  eusvnf  5293  reusv2lem4  5302  reusv2  5304  moop2  5392  elrnmpt1  5830  opabiota  6746  fvmptdf  6774  fmptco  6891  elabrex  7002  nfmpo  7236  cbvmpox  7247  ovmpodxf  7300  zfrep6  7656  fmpox  7765  nfwrecs  7949  erovlem  8393  xpf1o  8679  mapxpen  8683  wdom2d  9044  cnfcom3clem  9168  scott0  9315  cplem2  9319  infxpenc2lem2  9446  acnlem  9474  fin23lem32  9766  hsmexlem2  9849  axcc3  9860  ac6num  9901  lble  11593  nfsum1  15046  nfsumw  15047  nfsum  15048  zsum  15075  fsum  15077  fsumcvg2  15084  fsum2dlem  15125  infcvgaux1i  15212  nfcprod1  15264  nfcprod  15265  zprod  15291  fprod  15295  fprodser  15303  fprod2dlem  15334  cayleyhamilton1  21500  neiptopreu  21741  xkocnv  22422  istrkg2ld  26246  cnlnadjlem5  29848  chirred  30172  iundisjf  30339  opabdm  30362  opabrn  30363  dfimafnf  30381  fmptcof2  30402  mpomptxf  30425  f1od2  30457  fpwrelmap  30469  fedgmullem2  31026  esum2dlem  31351  oms0  31555  bnj1468  32118  bnj981  32222  bnj1463  32327  satfv1  32610  iota5f  32955  nfwlim  33109  nffrecs  33120  bj-seex  34244  isbasisrelowllem1  34639  isbasisrelowllem2  34640  exrecfnlem  34663  finxpreclem6  34680  phpreu  34891  matunitlindflem2  34904  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  mbfposadd  34954  itg2addnclem  34958  cover2  35004  indexa  35023  riotasvd  36107  cdleme31sn1  37532  cdleme32fva  37588  cdlemk36  38064  elnn0rabdioph  39449  wdom2d2  39681  elabrexg  41352  cbvmpo2  41412  cbvmpo1  41413  dffo3f  41487  elrnmptf  41490  disjrnmpt2  41498  fmuldfeqlem1  41912  climf  41952  climf2  41996  cncficcgt0  42220  stoweidlem8  42342  stoweidlem16  42350  stoweidlem19  42353  stoweidlem21  42355  stoweidlem22  42356  stoweidlem23  42357  stoweidlem29  42363  stoweidlem32  42366  stoweidlem35  42369  stoweidlem36  42370  stoweidlem41  42375  stoweidlem44  42378  stoweidlem45  42379  stoweidlem51  42385  stoweidlem53  42387  stoweidlem60  42394  fourierdlem80  42520  sprsymrelf  43706  cbvmpox2  44433  ovmpordxf  44436