Theorem nfeq2 2926

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 2922	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1537  Ⅎwnf 1781  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-cleq 2732  df-nfc 2895

This theorem is referenced by:  eqvincf  3663  csbhypf  3950  nfpr  4715  intab  5002  nfmpt  5273  cbvmptf  5275  cbvmptfg  5276  zfrepclf  5312  eusvnf  5410  reusv2lem4  5419  reusv2  5421  moop2  5521  elrnmpt1  5983  opabiota  7004  fvmptdf  7035  dffo3f  7140  fmptco  7163  elabrex  7279  elabrexg  7280  nfmpo  7532  cbvmpox  7543  ovmpodxf  7600  zfrep6  7995  fmpox  8108  nffrecs  8324  nfwrecsOLD  8358  erovlem  8871  xpf1o  9205  mapxpen  9209  wdom2d  9649  cnfcom3clem  9774  scott0  9955  cplem2  9959  infxpenc2lem2  10089  acnlem  10117  fin23lem32  10413  hsmexlem2  10496  axcc3  10507  ac6num  10548  lble  12247  nfsum1  15738  nfsum  15739  zsum  15766  fsum  15768  fsumcvg2  15775  fsum2dlem  15818  infcvgaux1i  15905  nfcprod1  15956  nfcprod  15957  zprod  15985  fprod  15989  fprodser  15997  fprod2dlem  16028  cayleyhamilton1  22919  neiptopreu  23162  xkocnv  23843  istrkg2ld  28486  cnlnadjlem5  32103  chirred  32427  iundisjf  32611  opabdm  32633  opabrn  32634  dfimafnf  32655  fmptcof2  32675  mpomptxf  32695  f1od2  32735  fpwrelmap  32747  elrspunidl  33421  fedgmullem2  33643  esum2dlem  34056  oms0  34262  bnj1468  34822  bnj981  34926  bnj1463  35031  satfv1  35331  iota5f  35686  nfwlim  35786  bj-seex  36888  isbasisrelowllem1  37321  isbasisrelowllem2  37322  exrecfnlem  37345  finxpreclem6  37362  phpreu  37564  matunitlindflem2  37577  poimirlem24  37604  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  mbfposadd  37627  itg2addnclem  37631  cover2  37675  indexa  37693  riotasvd  38912  cdleme31sn1  40338  cdleme32fva  40394  cdlemk36  40870  elnn0rabdioph  42759  wdom2d2  42992  cbvmpo2  44999  cbvmpo1  45000  elrnmptf  45088  disjrnmpt2  45095  fmuldfeqlem1  45503  climf  45543  climf2  45587  cncficcgt0  45809  stoweidlem8  45929  stoweidlem16  45937  stoweidlem19  45940  stoweidlem21  45942  stoweidlem22  45943  stoweidlem23  45944  stoweidlem29  45950  stoweidlem32  45953  stoweidlem35  45956  stoweidlem36  45957  stoweidlem41  45962  stoweidlem44  45965  stoweidlem45  45966  stoweidlem51  45972  stoweidlem53  45974  stoweidlem60  45981  fourierdlem80  46107  sprsymrelf  47369  cbvmpox2  48060  ovmpordxf  48063  1arymaptfo  48377  2arymaptfo  48388