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

Theorem nfeq2 2776
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 2761 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfeq 2772 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wnf 1705  wnfc 2748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-cleq 2614  df-nfc 2750
This theorem is referenced by:  issetf  3198  eqvincf  3319  csbhypf  3538  nfpr  4210  intab  4479  nfmpt  4716  cbvmptf  4718  cbvmpt  4719  zfrepclf  4747  eusvnf  4831  reusv2lem4  4842  reusv2  4844  moop2  4936  elrnmpt1  5344  opabiota  6228  fmptco  6362  elabrex  6466  nfmpt2  6689  cbvmpt2x  6698  ovmpt2dxf  6751  zfrep6  7096  fmpt2x  7196  nfwrecs  7369  erovlem  7803  xpf1o  8082  mapxpen  8086  wdom2d  8445  cnfcom3clem  8562  scott0  8709  cplem2  8713  infxpenc2lem2  8803  acnlem  8831  fin23lem32  9126  hsmexlem2  9209  axcc3  9220  ac6num  9261  lble  10935  nfsum1  14370  nfsum  14371  zsum  14398  fsum  14400  fsumcvg2  14407  fsum2dlem  14448  infcvgaux1i  14533  nfcprod1  14584  nfcprod  14585  zprod  14611  fprod  14615  fprodser  14623  fprod2dlem  14654  cayleyhamilton1  20637  neiptopreu  20877  xkocnv  21557  istrkg2ld  25293  cnlnadjlem5  28818  chirred  29142  iundisjf  29288  opabdm  29307  opabrn  29308  dfimafnf  29320  fmptcof2  29340  mpt2mptxf  29361  f1od2  29383  fpwrelmap  29392  esum2dlem  29977  oms0  30182  bnj1468  30677  bnj981  30781  bnj1463  30884  iota5f  31368  nfwlim  31522  bj-seex  32619  isbasisrelowllem1  32874  isbasisrelowllem2  32875  finxpreclem6  32904  phpreu  33064  matunitlindflem2  33077  poimirlem24  33104  poimirlem25  33105  poimirlem26  33106  poimirlem27  33107  mbfposadd  33128  itg2addnclem  33132  cover2  33179  indexa  33199  riotasvd  33761  cdleme31sn1  35188  cdleme32fva  35244  cdlemk36  35720  elnn0rabdioph  36886  wdom2d2  37121  elabrexg  38728  cbvmpt22  38799  cbvmpt21  38800  fmuldfeqlem1  39250  climf  39290  climf2  39334  cncficcgt0  39436  stoweidlem8  39562  stoweidlem16  39570  stoweidlem19  39573  stoweidlem21  39575  stoweidlem22  39576  stoweidlem23  39577  stoweidlem29  39583  stoweidlem32  39586  stoweidlem35  39589  stoweidlem36  39590  stoweidlem41  39595  stoweidlem44  39598  stoweidlem45  39599  stoweidlem51  39605  stoweidlem53  39607  stoweidlem60  39614  fourierdlem80  39740  sprsymrelf  41063  cbvmpt2x2  41432  ovmpt2rdxf  41435
  Copyright terms: Public domain W3C validator