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

Theorem nfeq2 2661
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 2646 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfeq 2657 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1468  wnf 1696  wnfc 2633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-ext 2485
This theorem depends on definitions:  df-bi 192  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-cleq 2498  df-nfc 2635
This theorem is referenced by:  issetf  3071  eqvincf  3190  csbhypf  3404  nfpr  4047  intab  4294  nfmpt  4524  cbvmptf  4526  cbvmpt  4527  zfrepclf  4554  eusvnf  4637  reusv2lem4  4646  reusv2  4648  moop2  4737  elrnmpt1  5132  opabiota  5995  fmptco  6124  elabrex  6219  nfmpt2  6435  cbvmpt2x  6444  ovmpt2dxf  6497  zfrep6  6838  fmpt2x  6936  nfwrecs  7107  erovlem  7541  xpf1o  7818  mapxpen  7822  wdom2d  8178  cnfcom3clem  8295  scott0  8442  cplem2  8446  infxpenc2lem2  8536  acnlem  8564  fin23lem32  8859  hsmexlem2  8942  axcc3  8953  ac6num  8994  lble  10647  nfsum1  13916  nfsum  13917  zsum  13944  fsum  13946  fsumcvg2  13953  fsum2dlem  13991  infcvgaux1i  14075  nfcprod1  14124  nfcprod  14125  zprod  14151  fprod  14155  fprodser  14163  fprod2dlem  14194  cayleyhamilton1  20074  neiptopreu  20306  xkocnv  20986  istrkg2ld  24669  cnlnadjlem5  27887  chirred  28211  iundisjf  28358  opabdm  28377  opabrn  28378  dfimafnf  28391  fmptcof2  28416  mpt2mptxf  28437  f1od2  28465  fpwrelmap  28474  esum2dlem  29068  oms0  29279  bnj1468  29809  bnj981  29913  bnj1463  30016  iota5f  30509  nfwlim  30656  bj-seex  31710  isbasisrelowllem1  31979  isbasisrelowllem2  31980  finxpreclem6  32009  phpreu  32162  matunitlindflem2  32175  poimirlem24  32202  poimirlem25  32203  poimirlem26  32204  poimirlem27  32205  mbfposadd  32226  itg2addnclem  32231  cover2  32278  indexa  32298  riotasvd  32761  cdleme31sn1  34188  cdleme32fva  34244  cdlemk36  34720  elnn0rabdioph  35886  wdom2d2  36130  elabrexg  37716  fmuldfeqlem1  38062  climf  38106  cncficcgt0  38175  stoweidlem8  38304  stoweidlem16  38312  stoweidlem19  38315  stoweidlem21  38317  stoweidlem22  38318  stoweidlem23  38319  stoweidlem29  38325  stoweidlem29OLD  38326  stoweidlem32  38329  stoweidlem35  38332  stoweidlem36  38333  stoweidlem41  38338  stoweidlem44  38341  stoweidlem45  38342  stoweidlem51  38348  stoweidlem53  38350  stoweidlem60  38357  fourierdlem80  38486  cbvmpt2x2  41307  ovmpt2rdxf  41310
  Copyright terms: Public domain W3C validator