Theorem nfeq2 2923

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

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

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 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2729  df-nfc 2892

This theorem is referenced by:  eqvincf  3650  csbhypf  3927  nfpr  4692  intab  4978  nfmpt  5249  cbvmptf  5251  cbvmptfg  5252  zfrepclf  5291  eusvnf  5392  reusv2lem4  5401  reusv2  5403  moop2  5507  elrnmpt1  5971  opabiota  6991  fvmptdf  7022  dffo3f  7126  fmptco  7149  elabrex  7262  elabrexg  7263  nfmpo  7515  cbvmpox  7526  ovmpodxf  7583  zfrep6  7979  fmpox  8092  nffrecs  8308  nfwrecsOLD  8342  erovlem  8853  xpf1o  9179  mapxpen  9183  wdom2d  9620  cnfcom3clem  9745  scott0  9926  cplem2  9930  infxpenc2lem2  10060  acnlem  10088  fin23lem32  10384  hsmexlem2  10467  axcc3  10478  ac6num  10519  lble  12220  nfsum1  15726  nfsum  15727  zsum  15754  fsum  15756  fsumcvg2  15763  fsum2dlem  15806  infcvgaux1i  15893  nfcprod1  15944  nfcprod  15945  zprod  15973  fprod  15977  fprodser  15985  fprod2dlem  16016  cayleyhamilton1  22898  neiptopreu  23141  xkocnv  23822  istrkg2ld  28468  cnlnadjlem5  32090  chirred  32414  iundisjf  32602  opabdm  32623  opabrn  32624  dfimafnf  32646  fmptcof2  32667  mpomptxf  32687  f1od2  32732  fpwrelmap  32744  elrgspnsubrunlem2  33252  elrspunidl  33456  fedgmullem2  33681  esum2dlem  34093  oms0  34299  bnj1468  34860  bnj981  34964  bnj1463  35069  satfv1  35368  iota5f  35724  nfwlim  35823  bj-seex  36923  isbasisrelowllem1  37356  isbasisrelowllem2  37357  exrecfnlem  37380  finxpreclem6  37397  phpreu  37611  matunitlindflem2  37624  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  mbfposadd  37674  itg2addnclem  37678  cover2  37722  indexa  37740  riotasvd  38957  cdleme31sn1  40383  cdleme32fva  40439  cdlemk36  40915  elnn0rabdioph  42814  wdom2d2  43047  cbvmpo2  45102  cbvmpo1  45103  elrnmptf  45186  disjrnmpt2  45193  fmuldfeqlem1  45597  climf  45637  climf2  45681  cncficcgt0  45903  stoweidlem8  46023  stoweidlem16  46031  stoweidlem19  46034  stoweidlem21  46036  stoweidlem22  46037  stoweidlem23  46038  stoweidlem29  46044  stoweidlem32  46047  stoweidlem35  46050  stoweidlem36  46051  stoweidlem41  46056  stoweidlem44  46059  stoweidlem45  46060  stoweidlem51  46066  stoweidlem53  46068  stoweidlem60  46075  fourierdlem80  46201  sprsymrelf  47482  cbvmpox2  48252  ovmpordxf  48255  1arymaptfo  48564  2arymaptfo  48575