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

Theorem nfeq2 2929
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 2913 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfeq 2925 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  wnf 1856  wnfc 2900
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-cleq 2764  df-nfc 2902
This theorem is referenced by:  issetf  3360  eqvincf  3482  csbhypf  3702  nfpr  4370  intab  4642  nfmpt  4881  cbvmptf  4883  cbvmpt  4884  zfrepclf  4912  eusvnf  4993  reusv2lem4  5002  reusv2  5004  moop2  5094  elrnmpt1  5513  opabiota  6404  fmptco  6540  elabrex  6645  nfmpt2  6872  cbvmpt2x  6881  ovmpt2dxf  6934  zfrep6  7282  fmpt2x  7387  nfwrecs  7562  erovlem  7997  xpf1o  8279  mapxpen  8283  wdom2d  8642  cnfcom3clem  8767  scott0  8914  cplem2  8918  infxpenc2lem2  9044  acnlem  9072  fin23lem32  9369  hsmexlem2  9452  axcc3  9463  ac6num  9504  lble  11178  nfsum1  14629  nfsum  14630  zsum  14658  fsum  14660  fsumcvg2  14667  fsum2dlem  14710  infcvgaux1i  14797  nfcprod1  14848  nfcprod  14849  zprod  14875  fprod  14879  fprodser  14887  fprod2dlem  14918  cayleyhamilton1  20918  neiptopreu  21159  xkocnv  21839  istrkg2ld  25581  cnlnadjlem5  29271  chirred  29595  iundisjf  29741  opabdm  29762  opabrn  29763  dfimafnf  29777  fmptcof2  29798  mpt2mptxf  29818  f1od2  29840  fpwrelmap  29849  esum2dlem  30495  oms0  30700  bnj1468  31255  bnj981  31359  bnj1463  31462  iota5f  31945  nfwlim  32105  nffrecs  32116  bj-seex  33251  isbasisrelowllem1  33541  isbasisrelowllem2  33542  finxpreclem6  33571  cnfinltrel  33579  phpreu  33727  matunitlindflem2  33740  poimirlem24  33767  poimirlem25  33768  poimirlem26  33769  poimirlem27  33770  mbfposadd  33790  itg2addnclem  33794  cover2  33841  indexa  33861  riotasvd  34765  cdleme31sn1  36191  cdleme32fva  36247  cdlemk36  36723  elnn0rabdioph  37894  wdom2d2  38129  elabrexg  39729  cbvmpt22  39799  cbvmpt21  39800  fmuldfeqlem1  40333  climf  40373  climf2  40417  cncficcgt0  40620  stoweidlem8  40743  stoweidlem16  40751  stoweidlem19  40754  stoweidlem21  40756  stoweidlem22  40757  stoweidlem23  40758  stoweidlem29  40764  stoweidlem32  40767  stoweidlem35  40770  stoweidlem36  40771  stoweidlem41  40776  stoweidlem44  40779  stoweidlem45  40780  stoweidlem51  40786  stoweidlem53  40788  stoweidlem60  40795  fourierdlem80  40921  sprsymrelf  42274  cbvmpt2x2  42643  ovmpt2rdxf  42646
  Copyright terms: Public domain W3C validator