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

Theorem nfeq2 2910
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 2894 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfeq 2906 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1624  wnf 1849  wnfc 2881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-ext 2732
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-cleq 2745  df-nfc 2883
This theorem is referenced by:  issetf  3340  eqvincf  3462  csbhypf  3685  nfpr  4368  intab  4651  nfmpt  4890  cbvmptf  4892  cbvmpt  4893  zfrepclf  4921  eusvnf  5002  reusv2lem4  5013  reusv2  5015  moop2  5106  elrnmpt1  5521  opabiota  6415  fmptco  6551  elabrex  6656  nfmpt2  6881  cbvmpt2x  6890  ovmpt2dxf  6943  zfrep6  7291  fmpt2x  7396  nfwrecs  7570  erovlem  8002  xpf1o  8279  mapxpen  8283  wdom2d  8642  cnfcom3clem  8767  scott0  8914  cplem2  8918  infxpenc2lem2  9025  acnlem  9053  fin23lem32  9350  hsmexlem2  9433  axcc3  9444  ac6num  9485  lble  11159  nfsum1  14611  nfsum  14612  zsum  14640  fsum  14642  fsumcvg2  14649  fsum2dlem  14692  infcvgaux1i  14780  nfcprod1  14831  nfcprod  14832  zprod  14858  fprod  14862  fprodser  14870  fprod2dlem  14901  cayleyhamilton1  20891  neiptopreu  21131  xkocnv  21811  istrkg2ld  25550  cnlnadjlem5  29231  chirred  29555  iundisjf  29701  opabdm  29722  opabrn  29723  dfimafnf  29737  fmptcof2  29758  mpt2mptxf  29778  f1od2  29800  fpwrelmap  29809  esum2dlem  30455  oms0  30660  bnj1468  31215  bnj981  31319  bnj1463  31422  iota5f  31905  nfwlim  32065  nffrecs  32076  bj-seex  33217  isbasisrelowllem1  33506  isbasisrelowllem2  33507  finxpreclem6  33536  cnfinltrel  33544  phpreu  33698  matunitlindflem2  33711  poimirlem24  33738  poimirlem25  33739  poimirlem26  33740  poimirlem27  33741  mbfposadd  33762  itg2addnclem  33766  cover2  33813  indexa  33833  riotasvd  34737  cdleme31sn1  36163  cdleme32fva  36219  cdlemk36  36695  elnn0rabdioph  37861  wdom2d2  38096  elabrexg  39697  cbvmpt22  39768  cbvmpt21  39769  fmuldfeqlem1  40309  climf  40349  climf2  40393  cncficcgt0  40596  stoweidlem8  40720  stoweidlem16  40728  stoweidlem19  40731  stoweidlem21  40733  stoweidlem22  40734  stoweidlem23  40735  stoweidlem29  40741  stoweidlem32  40744  stoweidlem35  40747  stoweidlem36  40748  stoweidlem41  40753  stoweidlem44  40756  stoweidlem45  40757  stoweidlem51  40763  stoweidlem53  40765  stoweidlem60  40772  fourierdlem80  40898  sprsymrelf  42247  cbvmpt2x2  42616  ovmpt2rdxf  42619
  Copyright terms: Public domain W3C validator