Theorem nfeq2 2995

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

Syntax hints:   = wceq 1537  Ⅎwnf 1784  Ⅎwnfc 2961

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 1970  ax-7 2015  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-cleq 2814  df-nfc 2963

This theorem is referenced by:  issetf  3507  eqvincf  3643  csbhypf  3911  nfpr  4628  intab  4906  nfmpt  5163  cbvmptf  5165  cbvmptfg  5166  zfrepclf  5198  eusvnf  5293  reusv2lem4  5302  reusv2  5304  moop2  5392  elrnmpt1  5830  opabiota  6746  fvmptdf  6774  fmptco  6891  elabrex  7002  nfmpo  7236  cbvmpox  7247  ovmpodxf  7300  zfrep6  7656  fmpox  7765  nfwrecs  7949  erovlem  8393  xpf1o  8679  mapxpen  8683  wdom2d  9044  cnfcom3clem  9168  scott0  9315  cplem2  9319  infxpenc2lem2  9446  acnlem  9474  fin23lem32  9766  hsmexlem2  9849  axcc3  9860  ac6num  9901  lble  11593  nfsum1  15046  nfsumw  15047  nfsum  15048  zsum  15075  fsum  15077  fsumcvg2  15084  fsum2dlem  15125  infcvgaux1i  15212  nfcprod1  15264  nfcprod  15265  zprod  15291  fprod  15295  fprodser  15303  fprod2dlem  15334  cayleyhamilton1  21500  neiptopreu  21741  xkocnv  22422  istrkg2ld  26246  cnlnadjlem5  29848  chirred  30172  iundisjf  30339  opabdm  30362  opabrn  30363  dfimafnf  30381  fmptcof2  30402  mpomptxf  30425  f1od2  30457  fpwrelmap  30469  fedgmullem2  31026  esum2dlem  31351  oms0  31555  bnj1468  32118  bnj981  32222  bnj1463  32327  satfv1  32610  iota5f  32955  nfwlim  33109  nffrecs  33120  bj-seex  34244  isbasisrelowllem1  34639  isbasisrelowllem2  34640  exrecfnlem  34663  finxpreclem6  34680  phpreu  34891  matunitlindflem2  34904  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  mbfposadd  34954  itg2addnclem  34958  cover2  35004  indexa  35023  riotasvd  36107  cdleme31sn1  37532  cdleme32fva  37588  cdlemk36  38064  elnn0rabdioph  39420  wdom2d2  39652  elabrexg  41323  cbvmpo2  41383  cbvmpo1  41384  dffo3f  41458  elrnmptf  41461  disjrnmpt2  41469  fmuldfeqlem1  41883  climf  41923  climf2  41967  cncficcgt0  42191  stoweidlem8  42313  stoweidlem16  42321  stoweidlem19  42324  stoweidlem21  42326  stoweidlem22  42327  stoweidlem23  42328  stoweidlem29  42334  stoweidlem32  42337  stoweidlem35  42340  stoweidlem36  42341  stoweidlem41  42346  stoweidlem44  42349  stoweidlem45  42350  stoweidlem51  42356  stoweidlem53  42358  stoweidlem60  42365  fourierdlem80  42491  sprsymrelf  43677  cbvmpox2  44404  ovmpordxf  44407