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

Theorem nfeq2 2551
Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq2.1  |-  F/_ x B
Assertion
Ref Expression
nfeq2  |-  F/ x  A  =  B
Distinct variable group:    x, A
Allowed substitution hint:    B( x)

Proof of Theorem nfeq2
StepHypRef Expression
1 nfcv 2540 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2547 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1550    = wceq 1649   F/_wnfc 2527
This theorem is referenced by:  issetf  2921  eqvincf  3024  csbhypf  3246  nfpr  3815  intab  4040  nfmpt  4257  cbvmpt  4259  zfrepclf  4286  moop2  4411  eusvnf  4677  reusv2lem4  4686  reusv2  4688  elrnmpt1  5078  fmptco  5860  zfrep6  5927  elabrex  5944  nfmpt2  6101  cbvmpt2x  6109  ovmpt2dxf  6158  fmpt2x  6376  opabiota  6497  riotasvd  6551  nfrecs  6594  erovlem  6959  xpf1o  7228  mapxpen  7232  wdom2d  7504  cnfcom3clem  7618  scott0  7766  cplem2  7770  infxpenc2lem2  7857  acnlem  7885  fin23lem32  8180  hsmexlem2  8263  axcc3  8274  ac6num  8315  lble  9916  nfsum1  12439  nfsum  12440  fsum  12469  fsumcvg2  12476  fsum2dlem  12509  infcvgaux1i  12591  neiptopreu  17152  xkocnv  17799  cnlnadjlem5  23527  chirred  23851  iundisjf  23982  dfimafnf  23996  cbvmptf  24021  fmptcof2  24029  iota5f  25135  nfcprod1  25189  nfcprod  25190  zprod  25216  fprod  25220  fprodser  25228  fprod2dlem  25257  itg2addnclem  26155  cover2  26305  indexa  26325  elnn0rabdioph  26753  wdom2d2  26996  fmuldfeqlem1  27579  stoweidlem8  27624  stoweidlem16  27632  stoweidlem19  27635  stoweidlem21  27637  stoweidlem22  27638  stoweidlem23  27639  stoweidlem29  27645  stoweidlem32  27648  stoweidlem35  27651  stoweidlem36  27652  stoweidlem41  27657  stoweidlem44  27660  stoweidlem45  27661  stoweidlem51  27667  stoweidlem53  27669  stoweidlem60  27676  bnj1468  28923  bnj981  29027  bnj1463  29130  cdleme31sn1  30863  cdleme32fva  30919  cdlemk36  31395
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529
  Copyright terms: Public domain W3C validator