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

Theorem nfeq2 2670
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 2655 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfeq 2666 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wnf 1698  wnfc 2642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-cleq 2507  df-nfc 2644
This theorem is referenced by:  issetf  3085  eqvincf  3205  csbhypf  3422  nfpr  4082  intab  4340  nfmpt  4572  cbvmptf  4574  cbvmpt  4575  zfrepclf  4603  eusvnf  4686  reusv2lem4  4697  reusv2  4699  moop2  4789  elrnmpt1  5186  opabiota  6054  fmptco  6186  elabrex  6281  nfmpt2  6498  cbvmpt2x  6507  ovmpt2dxf  6560  zfrep6  6901  fmpt2x  6999  nfwrecs  7170  erovlem  7605  xpf1o  7882  mapxpen  7886  wdom2d  8243  cnfcom3clem  8360  scott0  8507  cplem2  8511  infxpenc2lem2  8601  acnlem  8629  fin23lem32  8924  hsmexlem2  9007  axcc3  9018  ac6num  9059  lble  10724  nfsum1  14135  nfsum  14136  zsum  14163  fsum  14165  fsumcvg2  14172  fsum2dlem  14210  infcvgaux1i  14295  nfcprod1  14346  nfcprod  14347  zprod  14373  fprod  14377  fprodser  14385  fprod2dlem  14416  cayleyhamilton1  20417  neiptopreu  20648  xkocnv  21328  istrkg2ld  25049  cnlnadjlem5  28103  chirred  28427  iundisjf  28573  opabdm  28592  opabrn  28593  dfimafnf  28606  fmptcof2  28628  mpt2mptxf  28649  f1od2  28676  fpwrelmap  28685  esum2dlem  29278  oms0  29489  bnj1468  30016  bnj981  30120  bnj1463  30223  iota5f  30705  nfwlim  30851  bj-seex  31943  isbasisrelowllem1  32211  isbasisrelowllem2  32212  finxpreclem6  32241  phpreu  32438  matunitlindflem2  32451  poimirlem24  32478  poimirlem25  32479  poimirlem26  32480  poimirlem27  32481  mbfposadd  32502  itg2addnclem  32506  cover2  32553  indexa  32573  riotasvd  33135  cdleme31sn1  34562  cdleme32fva  34618  cdlemk36  35094  elnn0rabdioph  36260  wdom2d2  36495  elabrexg  38111  cbvmpt22  38188  cbvmpt21  38189  fmuldfeqlem1  38535  climf  38575  climf2  38620  cncficcgt0  38661  stoweidlem8  38791  stoweidlem16  38799  stoweidlem19  38802  stoweidlem21  38804  stoweidlem22  38805  stoweidlem23  38806  stoweidlem29  38812  stoweidlem32  38815  stoweidlem35  38818  stoweidlem36  38819  stoweidlem41  38824  stoweidlem44  38827  stoweidlem45  38828  stoweidlem51  38834  stoweidlem53  38836  stoweidlem60  38843  fourierdlem80  38971  cbvmpt2x2  41999  ovmpt2rdxf  42002
  Copyright terms: Public domain W3C validator