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

Theorem nfeq2 2765
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 2750 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfeq 2761 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wnf 1698  wnfc 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-cleq 2602  df-nfc 2739
This theorem is referenced by:  issetf  3180  eqvincf  3300  csbhypf  3517  nfpr  4178  intab  4436  nfmpt  4668  cbvmptf  4670  cbvmpt  4671  zfrepclf  4699  eusvnf  4782  reusv2lem4  4793  reusv2  4795  moop2  4885  elrnmpt1  5282  opabiota  6156  fmptco  6288  elabrex  6383  nfmpt2  6600  cbvmpt2x  6609  ovmpt2dxf  6662  zfrep6  7004  fmpt2x  7102  nfwrecs  7273  erovlem  7707  xpf1o  7984  mapxpen  7988  wdom2d  8345  cnfcom3clem  8462  scott0  8609  cplem2  8613  infxpenc2lem2  8703  acnlem  8731  fin23lem32  9026  hsmexlem2  9109  axcc3  9120  ac6num  9161  lble  10824  nfsum1  14214  nfsum  14215  zsum  14242  fsum  14244  fsumcvg2  14251  fsum2dlem  14289  infcvgaux1i  14374  nfcprod1  14425  nfcprod  14426  zprod  14452  fprod  14456  fprodser  14464  fprod2dlem  14495  cayleyhamilton1  20458  neiptopreu  20689  xkocnv  21369  istrkg2ld  25076  cnlnadjlem5  28120  chirred  28444  iundisjf  28590  opabdm  28609  opabrn  28610  dfimafnf  28623  fmptcof2  28645  mpt2mptxf  28666  f1od2  28693  fpwrelmap  28702  esum2dlem  29287  oms0  29492  bnj1468  29976  bnj981  30080  bnj1463  30183  iota5f  30667  nfwlim  30818  bj-seex  31907  isbasisrelowllem1  32175  isbasisrelowllem2  32176  finxpreclem6  32205  phpreu  32359  matunitlindflem2  32372  poimirlem24  32399  poimirlem25  32400  poimirlem26  32401  poimirlem27  32402  mbfposadd  32423  itg2addnclem  32427  cover2  32474  indexa  32494  riotasvd  33056  cdleme31sn1  34483  cdleme32fva  34539  cdlemk36  35015  elnn0rabdioph  36181  wdom2d2  36416  elabrexg  38025  cbvmpt22  38101  cbvmpt21  38102  fmuldfeqlem1  38446  climf  38486  climf2  38530  cncficcgt0  38571  stoweidlem8  38698  stoweidlem16  38706  stoweidlem19  38709  stoweidlem21  38711  stoweidlem22  38712  stoweidlem23  38713  stoweidlem29  38719  stoweidlem32  38722  stoweidlem35  38725  stoweidlem36  38726  stoweidlem41  38731  stoweidlem44  38734  stoweidlem45  38735  stoweidlem51  38741  stoweidlem53  38743  stoweidlem60  38750  fourierdlem80  38876  cbvmpt2x2  41902  ovmpt2rdxf  41905
  Copyright terms: Public domain W3C validator