Theorem nfeq2 2948

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

Syntax hints:   = wceq 1567  Ⅎwnf 1810  Ⅎwnfc 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-cleq 2761  df-nfc 2918

This theorem is referenced by:  eqvincf  3618  csbhypf  3889  nfpr  4663  intab  4947  nfmpt  5213  cbvmptf  5215  cbvmptfg  5216  zfrepclf  5256  eusvnf  5364  reusv2lem4  5373  reusv2  5375  moop2  5486  elrnmpt1  5951  opabiota  6964  fvmptdf  6997  dffo3f  7102  fmptco  7126  elabrex  7241  elabrexg  7242  nfmpo  7493  cbvmpox  7504  ovmpodxf  7561  zfrep6OLD  7951  fmpox  8063  nffrecs  8279  erovlem  8810  xpf1o  9126  mapxpen  9130  wdom2d  9541  cnfcom3clem  9673  scott0  9859  cplem2  9875  infxpenc2lem2  10003  acnlem  10031  fin23lem32  10327  hsmexlem2  10410  axcc3  10421  ac6num  10462  lble  12166  nfsum1  15740  nfsum  15741  zsum  15768  fsum  15770  fsumcvg2  15777  fsum2dlem  15820  infcvgaux1i  15910  nfcprod1  15961  nfcprod  15962  zprod  15990  fprod  15994  fprodser  16002  fprod2dlem  16033  cayleyhamilton1  23017  neiptopreu  23258  xkocnv  23939  istrkg2ld  28694  cnlnadjlem5  32363  chirred  32687  iundisjf  32874  opabdm  32896  opabrn  32897  dfimafnf  32921  fmptcof2  32942  mpomptxf  32963  f1od2  33004  fpwrelmap  33018  elrgspnsubrunlem2  33508  elrspunidl  33679  mplvrpmga  33879  esplyfval1  33907  fedgmullem2  33964  esum2dlem  34426  oms0  34631  bnj1468  35178  bnj981  35282  bnj1463  35387  satfv1  35753  iota5f  36114  nfwlim  36210  bj-seex  37445  isbasisrelowllem1  37888  isbasisrelowllem2  37889  exrecfnlem  37912  finxpreclem6  37929  phpreu  38142  matunitlindflem2  38155  poimirlem24  38182  poimirlem25  38183  poimirlem26  38184  poimirlem27  38185  mbfposadd  38205  itg2addnclem  38209  cover2  38253  indexa  38271  riotasvd  39619  cdleme31sn1  41044  cdleme32fva  41100  cdlemk36  41576  elnn0rabdioph  43421  wdom2d2  43653  permaxrep  45606  permaxsep  45607  cbvmpo2  45706  cbvmpo1  45707  elrnmptf  45790  disjrnmpt2  45797  fmuldfeqlem1  46189  climf  46229  climf2  46271  cncficcgt0  46493  stoweidlem8  46613  stoweidlem16  46621  stoweidlem19  46624  stoweidlem21  46626  stoweidlem22  46627  stoweidlem23  46628  stoweidlem29  46634  stoweidlem32  46637  stoweidlem35  46640  stoweidlem36  46641  stoweidlem41  46646  stoweidlem44  46649  stoweidlem45  46650  stoweidlem51  46656  stoweidlem53  46658  stoweidlem60  46665  fourierdlem80  46791  sprsymrelf  48132  cbvmpox2  49000  ovmpordxf  49003  1arymaptfo  49307  2arymaptfo  49318