Theorem nfeq2 2939

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

This proof depends on syntax axioms:   = wceq 1569  Ⅎwnf 1815  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-cleq 2752  df-nfc 2909

This theorem is used by:  eqvincf  3603  csbhypf  3875  nfpr  4649  intab  4937  nfmpt  5202  cbvmptf  5204  cbvmptfg  5205  zfrepclf  5243  eusvnf  5354  reusv2lem4  5363  reusv2  5365  moop2  5474  elrnmpt1  5943  opabiota  6972  fvmptdf  7005  dffo3f  7111  fmptco  7135  elabrex  7250  elabrexg  7251  nfmpo  7506  cbvmpox  7517  ovmpodxf  7574  zfrep6OLD  7971  fmpox  8082  f1od2  8114  nffrecs  8308  erovlem  8841  xpf1o  9165  mapxpen  9169  wdom2d  9581  cnfcom3clem  9713  scott0b  9944  scott0OLD  9945  cplem2  9959  cplem2OLD  9960  infxpenc2lem2  10106  acnlem  10134  fin23lem32  10429  hsmexlem2  10512  axcc3  10523  ac6num  10564  lble  12276  nfsum1  15866  nfsum  15867  zsum  15893  fsum  15895  fsumcvg2  15902  fsum2dlem  15945  infcvgaux1i  16035  nfcprod1  16086  nfcprod  16087  zprod  16113  fprod  16117  fprodser  16125  fprod2dlem  16156  matunitlindflem2  23004  cayleyhamilton1  23219  neiptopreu  23460  xkocnv  24142  istrkg2ld  28931  cnlnadjlem5  32682  chirred  33006  iundisjf  33234  opabdm  33256  opabrn  33257  dfimafnf  33281  fmptcof2  33302  mpomptxf  33323  fpwrelmap  33375  elrgspnsubrunlem2  33859  elrspunidl  34028  mplvrpmga  34227  esplyfval1  34255  fedgmullem2  34312  esum2dlem  34774  oms0  34979  bnj1468  35526  bnj981  35630  bnj1463  35735  srepdflem2  36009  satfv1  36218  iota5f  36585  nfwlim  36680  bj-seex  37930  isbasisrelowllem1  38387  isbasisrelowllem2  38388  exrecfnlem  38411  finxpreclem6  38428  phpreu  38636  poimirlem24  38671  poimirlem25  38672  poimirlem26  38673  poimirlem27  38674  mbfposadd  38694  itg2addnclem  38698  cover2  38758  indexa  38776  riotasvd  40122  cdleme31sn1  41547  cdleme32fva  41603  cdlemk36  42079  elnn0rabdioph  43919  wdom2d2  44151  permaxrep  46104  permaxsep  46105  cbvmpo2  46220  cbvmpo1  46221  elrnmptf  46304  disjrnmpt2  46311  fmuldfeqlem1  46702  climf  46742  climf2  46784  cncficcgt0  47006  stoweidlem8  47126  stoweidlem16  47134  stoweidlem19  47137  stoweidlem21  47139  stoweidlem22  47140  stoweidlem23  47141  stoweidlem29  47147  stoweidlem32  47150  stoweidlem35  47153  stoweidlem36  47154  stoweidlem41  47159  stoweidlem44  47162  stoweidlem45  47163  stoweidlem51  47169  stoweidlem53  47171  stoweidlem60  47178  fourierdlem80  47304  sprsymrelf  48685  cbvmpox2  49556  ovmpordxf  49559  1arymaptfo  49863  2arymaptfo  49874