MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfeq2 Structured version   Visualization version   GIF version

Theorem nfeq2 2766
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
StepHypRef Expression
1 nfcv 2751 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfeq 2762 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1475  wnf 1699  wnfc 2738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-nfc 2740
This theorem is referenced by:  issetf  3181  eqvincf  3301  csbhypf  3518  nfpr  4179  intab  4442  nfmpt  4674  cbvmptf  4676  cbvmpt  4677  zfrepclf  4705  eusvnf  4787  reusv2lem4  4798  reusv2  4800  moop2  4891  elrnmpt1  5295  opabiota  6171  fmptco  6303  elabrex  6405  nfmpt2  6622  cbvmpt2x  6631  ovmpt2dxf  6684  zfrep6  7027  fmpt2x  7125  nfwrecs  7296  erovlem  7730  xpf1o  8007  mapxpen  8011  wdom2d  8368  cnfcom3clem  8485  scott0  8632  cplem2  8636  infxpenc2lem2  8726  acnlem  8754  fin23lem32  9049  hsmexlem2  9132  axcc3  9143  ac6num  9184  lble  10854  nfsum1  14268  nfsum  14269  zsum  14296  fsum  14298  fsumcvg2  14305  fsum2dlem  14343  infcvgaux1i  14428  nfcprod1  14479  nfcprod  14480  zprod  14506  fprod  14510  fprodser  14518  fprod2dlem  14549  cayleyhamilton1  20516  neiptopreu  20747  xkocnv  21427  istrkg2ld  25159  cnlnadjlem5  28314  chirred  28638  iundisjf  28784  opabdm  28803  opabrn  28804  dfimafnf  28817  fmptcof2  28839  mpt2mptxf  28860  f1od2  28887  fpwrelmap  28896  esum2dlem  29481  oms0  29686  bnj1468  30170  bnj981  30274  bnj1463  30377  iota5f  30861  nfwlim  31012  bj-seex  32111  isbasisrelowllem1  32379  isbasisrelowllem2  32380  finxpreclem6  32409  phpreu  32563  matunitlindflem2  32576  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  mbfposadd  32627  itg2addnclem  32631  cover2  32678  indexa  32698  riotasvd  33260  cdleme31sn1  34687  cdleme32fva  34743  cdlemk36  35219  elnn0rabdioph  36385  wdom2d2  36620  elabrexg  38229  cbvmpt22  38305  cbvmpt21  38306  fmuldfeqlem1  38649  climf  38689  climf2  38733  cncficcgt0  38774  stoweidlem8  38901  stoweidlem16  38909  stoweidlem19  38912  stoweidlem21  38914  stoweidlem22  38915  stoweidlem23  38916  stoweidlem29  38922  stoweidlem32  38925  stoweidlem35  38928  stoweidlem36  38929  stoweidlem41  38934  stoweidlem44  38937  stoweidlem45  38938  stoweidlem51  38944  stoweidlem53  38946  stoweidlem60  38953  fourierdlem80  39079  cbvmpt2x2  41907  ovmpt2rdxf  41910
  Copyright terms: Public domain W3C validator