Theorem nfeq2 2940

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

This proof depends on syntax axioms:   = wceq 1570  Ⅎwnf 1816  Ⅎwnfc 2908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-cleq 2753  df-nfc 2910

This theorem is used by:  eqvincf  3604  csbhypf  3875  nfpr  4653  intab  4938  nfmpt  5203  cbvmptf  5205  cbvmptfg  5206  zfrepclf  5244  eusvnf  5354  reusv2lem4  5363  reusv2  5365  moop2  5474  elrnmpt1  5942  opabiota  6965  fvmptdf  6998  dffo3f  7104  fmptco  7128  elabrex  7244  elabrexg  7245  nfmpo  7500  cbvmpox  7511  ovmpodxf  7568  zfrep6OLD  7965  fmpox  8076  nffrecs  8294  erovlem  8827  xpf1o  9151  mapxpen  9155  wdom2d  9567  cnfcom3clem  9699  scott0b  9930  scott0OLD  9931  cplem2  9945  cplem2OLD  9946  infxpenc2lem2  10092  acnlem  10120  fin23lem32  10415  hsmexlem2  10498  axcc3  10509  ac6num  10550  lble  12262  nfsum1  15850  nfsum  15851  zsum  15877  fsum  15879  fsumcvg2  15886  fsum2dlem  15929  infcvgaux1i  16019  nfcprod1  16070  nfcprod  16071  zprod  16097  fprod  16101  fprodser  16109  fprod2dlem  16140  matunitlindflem2  22988  cayleyhamilton1  23203  neiptopreu  23444  xkocnv  24126  istrkg2ld  28915  cnlnadjlem5  32666  chirred  32990  iundisjf  33176  opabdm  33198  opabrn  33199  dfimafnf  33223  fmptcof2  33244  mpomptxf  33265  f1od2  33304  fpwrelmap  33318  elrgspnsubrunlem2  33802  elrspunidl  33971  mplvrpmga  34170  esplyfval1  34198  fedgmullem2  34255  esum2dlem  34717  oms0  34922  bnj1468  35469  bnj981  35573  bnj1463  35678  satfv1  36107  iota5f  36468  nfwlim  36564  bj-seex  37814  isbasisrelowllem1  38258  isbasisrelowllem2  38259  exrecfnlem  38282  finxpreclem6  38299  phpreu  38507  poimirlem24  38542  poimirlem25  38543  poimirlem26  38544  poimirlem27  38545  mbfposadd  38565  itg2addnclem  38569  cover2  38629  indexa  38647  riotasvd  39993  cdleme31sn1  41418  cdleme32fva  41474  cdlemk36  41950  elnn0rabdioph  43789  wdom2d2  44021  permaxrep  45974  permaxsep  45975  cbvmpo2  46081  cbvmpo1  46082  elrnmptf  46165  disjrnmpt2  46172  fmuldfeqlem1  46563  climf  46603  climf2  46645  cncficcgt0  46867  stoweidlem8  46987  stoweidlem16  46995  stoweidlem19  46998  stoweidlem21  47000  stoweidlem22  47001  stoweidlem23  47002  stoweidlem29  47008  stoweidlem32  47011  stoweidlem35  47014  stoweidlem36  47015  stoweidlem41  47020  stoweidlem44  47023  stoweidlem45  47024  stoweidlem51  47030  stoweidlem53  47032  stoweidlem60  47039  fourierdlem80  47165  sprsymrelf  48546  cbvmpox2  49417  ovmpordxf  49420  1arymaptfo  49724  2arymaptfo  49735