Theorem nfeq2 2949

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

Syntax hints:   = wceq 1601  Ⅎwnf 1827  Ⅎwnfc 2919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-cleq 2770  df-nfc 2921

This theorem is referenced by:  issetf  3410  eqvincf  3534  csbhypf  3770  nfpr  4459  intab  4742  nfmpt  4983  cbvmptf  4985  cbvmpt  4986  zfrepclf  5015  eusvnf  5106  reusv2lem4  5115  reusv2  5117  moop2  5199  elrnmpt1  5622  opabiota  6523  fmptco  6663  elabrex  6775  nfmpt2  7003  cbvmpt2x  7012  ovmpt2dxf  7065  zfrep6  7415  fmpt2x  7518  nfwrecs  7693  erovlem  8129  xpf1o  8412  mapxpen  8416  wdom2d  8776  cnfcom3clem  8901  scott0  9048  cplem2  9052  infxpenc2lem2  9178  acnlem  9206  fin23lem32  9503  hsmexlem2  9586  axcc3  9597  ac6num  9638  lble  11334  nfsum1  14837  nfsum  14838  zsum  14865  fsum  14867  fsumcvg2  14874  fsum2dlem  14915  infcvgaux1i  15002  nfcprod1  15052  nfcprod  15053  zprod  15079  fprod  15083  fprodser  15091  fprod2dlem  15122  cayleyhamilton1  21115  neiptopreu  21356  xkocnv  22037  istrkg2ld  25828  cnlnadjlem5  29519  chirred  29843  iundisjf  29982  opabdm  30003  opabrn  30004  dfimafnf  30018  fmptcof2  30039  mpt2mptxf  30060  f1od2  30082  fpwrelmap  30091  esum2dlem  30760  oms0  30965  bnj1468  31523  bnj981  31627  bnj1463  31730  iota5f  32211  nfwlim  32364  nffrecs  32375  bj-seex  33500  isbasisrelowllem1  33805  isbasisrelowllem2  33806  finxpreclem6  33835  cnfinltrel  33843  phpreu  34027  matunitlindflem2  34041  poimirlem24  34068  poimirlem25  34069  poimirlem26  34070  poimirlem27  34071  mbfposadd  34091  itg2addnclem  34095  cover2  34142  indexa  34162  riotasvd  35119  cdleme31sn1  36544  cdleme32fva  36600  cdlemk36  37076  elnn0rabdioph  38341  wdom2d2  38575  elabrexg  40153  cbvmpt22  40222  cbvmpt21  40223  fmuldfeqlem1  40736  climf  40776  climf2  40820  cncficcgt0  41043  stoweidlem8  41166  stoweidlem16  41174  stoweidlem19  41177  stoweidlem21  41179  stoweidlem22  41180  stoweidlem23  41181  stoweidlem29  41187  stoweidlem32  41190  stoweidlem35  41193  stoweidlem36  41194  stoweidlem41  41199  stoweidlem44  41202  stoweidlem45  41203  stoweidlem51  41209  stoweidlem53  41211  stoweidlem60  41218  fourierdlem80  41344  sprsymrelf  42448  cbvmpt2x2  43143  ovmpt2rdxf  43146