Theorem nfeq2 2914

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

Syntax hints:   = wceq 1541  Ⅎwnf 1784  Ⅎwnfc 2881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2726  df-nfc 2883

This theorem is referenced by:  eqvincf  3602  csbhypf  3875  nfpr  4647  intab  4931  nfmpt  5194  cbvmptf  5196  cbvmptfg  5197  zfrepclf  5234  eusvnf  5335  reusv2lem4  5344  reusv2  5346  moop2  5448  elrnmpt1  5907  opabiota  6914  fvmptdf  6945  dffo3f  7049  fmptco  7072  elabrex  7186  elabrexg  7187  nfmpo  7438  cbvmpox  7449  ovmpodxf  7506  zfrep6  7897  fmpox  8009  nffrecs  8223  erovlem  8748  xpf1o  9065  mapxpen  9069  wdom2d  9483  cnfcom3clem  9612  scott0  9796  cplem2  9800  infxpenc2lem2  9928  acnlem  9956  fin23lem32  10252  hsmexlem2  10335  axcc3  10346  ac6num  10387  lble  12092  nfsum1  15611  nfsum  15612  zsum  15639  fsum  15641  fsumcvg2  15648  fsum2dlem  15691  infcvgaux1i  15778  nfcprod1  15829  nfcprod  15830  zprod  15858  fprod  15862  fprodser  15870  fprod2dlem  15901  cayleyhamilton1  22834  neiptopreu  23075  xkocnv  23756  istrkg2ld  28481  cnlnadjlem5  32095  chirred  32419  iundisjf  32613  opabdm  32638  opabrn  32639  dfimafnf  32663  fmptcof2  32684  mpomptxf  32706  f1od2  32747  fpwrelmap  32761  elrgspnsubrunlem2  33279  elrspunidl  33458  mplvrpmga  33659  fedgmullem2  33736  esum2dlem  34198  oms0  34403  bnj1468  34951  bnj981  35055  bnj1463  35160  satfv1  35506  iota5f  35867  nfwlim  35963  bj-seex  37066  isbasisrelowllem1  37499  isbasisrelowllem2  37500  exrecfnlem  37523  finxpreclem6  37540  phpreu  37744  matunitlindflem2  37757  poimirlem24  37784  poimirlem25  37785  poimirlem26  37786  poimirlem27  37787  mbfposadd  37807  itg2addnclem  37811  cover2  37855  indexa  37873  riotasvd  39155  cdleme31sn1  40580  cdleme32fva  40636  cdlemk36  41112  elnn0rabdioph  42987  wdom2d2  43219  permaxrep  45189  permaxsep  45190  cbvmpo2  45283  cbvmpo1  45284  elrnmptf  45367  disjrnmpt2  45374  fmuldfeqlem1  45770  climf  45810  climf2  45852  cncficcgt0  46074  stoweidlem8  46194  stoweidlem16  46202  stoweidlem19  46205  stoweidlem21  46207  stoweidlem22  46208  stoweidlem23  46209  stoweidlem29  46215  stoweidlem32  46218  stoweidlem35  46221  stoweidlem36  46222  stoweidlem41  46227  stoweidlem44  46230  stoweidlem45  46231  stoweidlem51  46237  stoweidlem53  46239  stoweidlem60  46246  fourierdlem80  46372  sprsymrelf  47683  cbvmpox2  48524  ovmpordxf  48527  1arymaptfo  48831  2arymaptfo  48842