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

Theorem nfeq2 2636
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:   ,

Proof of Theorem nfeq2
StepHypRef Expression
1 nfcv 2619 . 2
2 nfeq2.1 . 2
31, 2nfeq 2630 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  F/wnf 1616  F/_wnfc 2605
This theorem is referenced by:  issetf  3114  eqvincf  3227  csbhypf  3453  nfpr  4076  intab  4317  nfmpt  4540  cbvmpt  4542  zfrepclf  4569  eusvnf  4647  reusv2lem4  4656  reusv2  4658  moop2  4747  elrnmpt1  5256  opabiota  5936  fmptco  6064  elabrex  6155  nfmpt2  6366  cbvmpt2x  6375  ovmpt2dxf  6428  zfrep6  6768  fmpt2x  6866  nfrecs  7063  erovlem  7426  xpf1o  7699  mapxpen  7703  wdom2d  8027  cnfcom3clem  8170  cnfcom3clemOLD  8178  scott0  8325  cplem2  8329  infxpenc2lem2  8418  infxpenc2lem2OLD  8422  acnlem  8450  fin23lem32  8745  hsmexlem2  8828  axcc3  8839  ac6num  8880  lble  10520  nfsum1  13512  nfsum  13513  zsum  13540  fsum  13542  fsumcvg2  13549  fsum2dlem  13585  infcvgaux1i  13668  nfcprod1  13717  nfcprod  13718  zprod  13744  fprod  13748  fprodser  13756  fprod2dlem  13784  cayleyhamilton1  19393  neiptopreu  19634  xkocnv  20315  istrkg2ld  23858  cnlnadjlem5  26990  chirred  27314  iundisjf  27448  opabdm  27464  opabrn  27465  dfimafnf  27473  cbvmptf  27494  fmptcof2  27502  mpt2mptxf  27518  f1od2  27547  fpwrelmap  27556  oms0  28266  iota5f  29102  nfwrecs  29338  nfwlim  29378  mbfposadd  30062  itg2addnclem  30066  cover2  30204  indexa  30224  elnn0rabdioph  30736  wdom2d2  30977  elabrexg  31430  fmuldfeqlem1  31576  climf  31628  cncficcgt0  31691  stoweidlem8  31790  stoweidlem16  31798  stoweidlem19  31801  stoweidlem21  31803  stoweidlem22  31804  stoweidlem23  31805  stoweidlem29  31811  stoweidlem32  31814  stoweidlem35  31817  stoweidlem36  31818  stoweidlem41  31823  stoweidlem44  31826  stoweidlem45  31827  stoweidlem51  31833  stoweidlem53  31835  stoweidlem60  31842  fourierdlem80  31969  cbvmpt2x2  32925  ovmpt2rdxf  32928  bnj1468  33904  bnj981  34008  bnj1463  34111  bj-seex  34491  riotasvd  34687  cdleme31sn1  36107  cdleme32fva  36163  cdlemk36  36639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-nfc 2607
  Copyright terms: Public domain W3C validator