Theorem nfeq2 2916

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

Syntax hints:   = wceq 1540  Ⅎwnf 1783  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2727  df-nfc 2885

This theorem is referenced by:  eqvincf  3629  csbhypf  3902  nfpr  4668  intab  4954  nfmpt  5219  cbvmptf  5221  cbvmptfg  5222  zfrepclf  5261  eusvnf  5362  reusv2lem4  5371  reusv2  5373  moop2  5477  elrnmpt1  5940  opabiota  6960  fvmptdf  6991  dffo3f  7095  fmptco  7118  elabrex  7233  elabrexg  7234  nfmpo  7487  cbvmpox  7498  ovmpodxf  7555  zfrep6  7951  fmpox  8064  nffrecs  8280  nfwrecsOLD  8314  erovlem  8825  xpf1o  9151  mapxpen  9155  wdom2d  9592  cnfcom3clem  9717  scott0  9898  cplem2  9902  infxpenc2lem2  10032  acnlem  10060  fin23lem32  10356  hsmexlem2  10439  axcc3  10450  ac6num  10491  lble  12192  nfsum1  15704  nfsum  15705  zsum  15732  fsum  15734  fsumcvg2  15741  fsum2dlem  15784  infcvgaux1i  15871  nfcprod1  15922  nfcprod  15923  zprod  15951  fprod  15955  fprodser  15963  fprod2dlem  15994  cayleyhamilton1  22828  neiptopreu  23069  xkocnv  23750  istrkg2ld  28385  cnlnadjlem5  31998  chirred  32322  iundisjf  32516  opabdm  32537  opabrn  32538  dfimafnf  32560  fmptcof2  32581  mpomptxf  32601  f1od2  32644  fpwrelmap  32656  elrgspnsubrunlem2  33189  elrspunidl  33389  fedgmullem2  33616  esum2dlem  34069  oms0  34275  bnj1468  34823  bnj981  34927  bnj1463  35032  satfv1  35331  iota5f  35687  nfwlim  35786  bj-seex  36886  isbasisrelowllem1  37319  isbasisrelowllem2  37320  exrecfnlem  37343  finxpreclem6  37360  phpreu  37574  matunitlindflem2  37587  poimirlem24  37614  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  mbfposadd  37637  itg2addnclem  37641  cover2  37685  indexa  37703  riotasvd  38920  cdleme31sn1  40346  cdleme32fva  40402  cdlemk36  40878  elnn0rabdioph  42773  wdom2d2  43006  permaxrep  44979  permaxsep  44980  cbvmpo2  45069  cbvmpo1  45070  elrnmptf  45153  disjrnmpt2  45160  fmuldfeqlem1  45559  climf  45599  climf2  45643  cncficcgt0  45865  stoweidlem8  45985  stoweidlem16  45993  stoweidlem19  45996  stoweidlem21  45998  stoweidlem22  45999  stoweidlem23  46000  stoweidlem29  46006  stoweidlem32  46009  stoweidlem35  46012  stoweidlem36  46013  stoweidlem41  46018  stoweidlem44  46021  stoweidlem45  46022  stoweidlem51  46028  stoweidlem53  46030  stoweidlem60  46037  fourierdlem80  46163  sprsymrelf  47457  cbvmpox2  48259  ovmpordxf  48262  1arymaptfo  48571  2arymaptfo  48582