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

Theorem nfeq2 2776
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 2761 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfeq 2772 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wnf 1705  wnfc 2748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-cleq 2614  df-nfc 2750
This theorem is referenced by:  issetf  3194  eqvincf  3314  csbhypf  3533  nfpr  4203  intab  4472  nfmpt  4706  cbvmptf  4708  cbvmpt  4709  zfrepclf  4737  eusvnf  4821  reusv2lem4  4832  reusv2  4834  moop2  4926  elrnmpt1  5334  opabiota  6218  fmptco  6351  elabrex  6455  nfmpt2  6677  cbvmpt2x  6686  ovmpt2dxf  6739  zfrep6  7081  fmpt2x  7181  nfwrecs  7354  erovlem  7788  xpf1o  8066  mapxpen  8070  wdom2d  8429  cnfcom3clem  8546  scott0  8693  cplem2  8697  infxpenc2lem2  8787  acnlem  8815  fin23lem32  9110  hsmexlem2  9193  axcc3  9204  ac6num  9245  lble  10919  nfsum1  14354  nfsum  14355  zsum  14382  fsum  14384  fsumcvg2  14391  fsum2dlem  14429  infcvgaux1i  14514  nfcprod1  14565  nfcprod  14566  zprod  14592  fprod  14596  fprodser  14604  fprod2dlem  14635  cayleyhamilton1  20616  neiptopreu  20847  xkocnv  21527  istrkg2ld  25259  cnlnadjlem5  28779  chirred  29103  iundisjf  29247  opabdm  29266  opabrn  29267  dfimafnf  29279  fmptcof2  29299  mpt2mptxf  29320  f1od2  29342  fpwrelmap  29351  esum2dlem  29935  oms0  30140  bnj1468  30624  bnj981  30728  bnj1463  30831  iota5f  31315  nfwlim  31469  bj-seex  32566  isbasisrelowllem1  32835  isbasisrelowllem2  32836  finxpreclem6  32865  phpreu  33025  matunitlindflem2  33038  poimirlem24  33065  poimirlem25  33066  poimirlem26  33067  poimirlem27  33068  mbfposadd  33089  itg2addnclem  33093  cover2  33140  indexa  33160  riotasvd  33722  cdleme31sn1  35149  cdleme32fva  35205  cdlemk36  35681  elnn0rabdioph  36847  wdom2d2  37082  elabrexg  38689  cbvmpt22  38762  cbvmpt21  38763  fmuldfeqlem1  39218  climf  39258  climf2  39302  cncficcgt0  39405  stoweidlem8  39532  stoweidlem16  39540  stoweidlem19  39543  stoweidlem21  39545  stoweidlem22  39546  stoweidlem23  39547  stoweidlem29  39553  stoweidlem32  39556  stoweidlem35  39559  stoweidlem36  39560  stoweidlem41  39565  stoweidlem44  39568  stoweidlem45  39569  stoweidlem51  39575  stoweidlem53  39577  stoweidlem60  39584  fourierdlem80  39710  sprsymrelf  41033  cbvmpt2x2  41402  ovmpt2rdxf  41405
  Copyright terms: Public domain W3C validator