Theorem nfeq2 2949

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

Syntax hints:   = wceq 1568  Ⅎwnf 1811  Ⅎwnfc 2917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-9 2160  ax-10 2183  ax-11 2199  ax-12 2220  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-nf 1812  df-cleq 2762  df-nfc 2919

This theorem is referenced by:  eqvincf  3617  csbhypf  3889  nfpr  4663  intab  4948  nfmpt  5214  cbvmptf  5216  cbvmptfg  5217  zfrepclf  5257  eusvnf  5367  reusv2lem4  5376  reusv2  5378  moop2  5489  elrnmpt1  5954  opabiota  6967  fvmptdf  7000  dffo3f  7105  fmptco  7129  elabrex  7244  elabrexg  7245  nfmpo  7496  cbvmpox  7507  ovmpodxf  7564  zfrep6OLD  7955  fmpox  8067  nffrecs  8283  erovlem  8814  xpf1o  9130  mapxpen  9134  wdom2d  9545  cnfcom3clem  9677  scott0  9863  cplem2  9879  infxpenc2lem2  10007  acnlem  10035  fin23lem32  10331  hsmexlem2  10414  axcc3  10425  ac6num  10466  lble  12170  nfsum1  15744  nfsum  15745  zsum  15772  fsum  15774  fsumcvg2  15781  fsum2dlem  15824  infcvgaux1i  15914  nfcprod1  15965  nfcprod  15966  zprod  15994  fprod  15998  fprodser  16006  fprod2dlem  16037  cayleyhamilton1  23032  neiptopreu  23273  xkocnv  23954  istrkg2ld  28709  cnlnadjlem5  32393  chirred  32717  iundisjf  32904  opabdm  32926  opabrn  32927  dfimafnf  32951  fmptcof2  32972  mpomptxf  32993  f1od2  33034  fpwrelmap  33048  elrgspnsubrunlem2  33538  elrspunidl  33706  mplvrpmga  33905  esplyfval1  33933  fedgmullem2  33990  esum2dlem  34452  oms0  34657  bnj1468  35204  bnj981  35308  bnj1463  35413  satfv1  35813  iota5f  36174  nfwlim  36270  bj-seex  37505  isbasisrelowllem1  37949  isbasisrelowllem2  37950  exrecfnlem  37973  finxpreclem6  37990  phpreu  38203  matunitlindflem2  38216  poimirlem24  38243  poimirlem25  38244  poimirlem26  38245  poimirlem27  38246  mbfposadd  38266  itg2addnclem  38270  cover2  38314  indexa  38332  riotasvd  39680  cdleme31sn1  41105  cdleme32fva  41161  cdlemk36  41637  elnn0rabdioph  43482  wdom2d2  43714  permaxrep  45667  permaxsep  45668  cbvmpo2  45767  cbvmpo1  45768  elrnmptf  45851  disjrnmpt2  45858  fmuldfeqlem1  46250  climf  46290  climf2  46332  cncficcgt0  46554  stoweidlem8  46674  stoweidlem16  46682  stoweidlem19  46685  stoweidlem21  46687  stoweidlem22  46688  stoweidlem23  46689  stoweidlem29  46695  stoweidlem32  46698  stoweidlem35  46701  stoweidlem36  46702  stoweidlem41  46707  stoweidlem44  46710  stoweidlem45  46711  stoweidlem51  46717  stoweidlem53  46719  stoweidlem60  46726  fourierdlem80  46852  sprsymrelf  48193  cbvmpox2  49065  ovmpordxf  49068  1arymaptfo  49372  2arymaptfo  49383