Theorem nfeq2 2925

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

Syntax hints:   = wceq 1539  Ⅎwnf 1786  Ⅎwnfc 2888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-cleq 2731  df-nfc 2890

This theorem is referenced by:  issetf  3447  eqvincf  3581  csbhypf  3862  nfpr  4627  intab  4910  nfmpt  5182  cbvmptf  5184  cbvmptfg  5185  zfrepclf  5219  eusvnf  5316  reusv2lem4  5325  reusv2  5327  moop2  5417  elrnmpt1  5870  opabiota  6860  fvmptdf  6890  fmptco  7010  elabrex  7125  nfmpo  7366  cbvmpox  7377  ovmpodxf  7432  zfrep6  7806  fmpox  7916  nffrecs  8108  nfwrecsOLD  8142  erovlem  8611  xpf1o  8935  mapxpen  8939  wdom2d  9348  cnfcom3clem  9472  scott0  9653  cplem2  9657  infxpenc2lem2  9785  acnlem  9813  fin23lem32  10109  hsmexlem2  10192  axcc3  10203  ac6num  10244  lble  11936  nfsum1  15410  nfsum  15411  nfsumOLD  15412  zsum  15439  fsum  15441  fsumcvg2  15448  fsum2dlem  15491  infcvgaux1i  15578  nfcprod1  15629  nfcprod  15630  zprod  15656  fprod  15660  fprodser  15668  fprod2dlem  15699  cayleyhamilton1  22050  neiptopreu  22293  xkocnv  22974  istrkg2ld  26830  cnlnadjlem5  30442  chirred  30766  iundisjf  30937  opabdm  30960  opabrn  30961  dfimafnf  30980  fmptcof2  31003  mpomptxf  31025  f1od2  31065  fpwrelmap  31077  elrspunidl  31615  fedgmullem2  31720  esum2dlem  32069  oms0  32273  bnj1468  32835  bnj981  32939  bnj1463  33044  satfv1  33334  iota5f  33678  nfwlim  33825  bj-seex  35119  isbasisrelowllem1  35535  isbasisrelowllem2  35536  exrecfnlem  35559  finxpreclem6  35576  phpreu  35770  matunitlindflem2  35783  poimirlem24  35810  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  mbfposadd  35833  itg2addnclem  35837  cover2  35881  indexa  35900  riotasvd  36977  cdleme31sn1  38402  cdleme32fva  38458  cdlemk36  38934  elnn0rabdioph  40632  wdom2d2  40864  elabrexg  42596  cbvmpo2  42654  cbvmpo1  42655  dffo3f  42724  elrnmptf  42725  disjrnmpt2  42733  fmuldfeqlem1  43130  climf  43170  climf2  43214  cncficcgt0  43436  stoweidlem8  43556  stoweidlem16  43564  stoweidlem19  43567  stoweidlem21  43569  stoweidlem22  43570  stoweidlem23  43571  stoweidlem29  43577  stoweidlem32  43580  stoweidlem35  43583  stoweidlem36  43584  stoweidlem41  43589  stoweidlem44  43592  stoweidlem45  43593  stoweidlem51  43599  stoweidlem53  43601  stoweidlem60  43608  fourierdlem80  43734  sprsymrelf  44958  cbvmpox2  45682  ovmpordxf  45685  1arymaptfo  46000  2arymaptfo  46011