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

Theorem nfeq2 2577
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 2566 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2573 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1553    = wceq 1652   F/_wnfc 2553
This theorem is referenced by:  issetf  2948  eqvincf  3051  csbhypf  3273  nfpr  3842  intab  4067  nfmpt  4284  cbvmpt  4286  zfrepclf  4313  moop2  4438  eusvnf  4704  reusv2lem4  4713  reusv2  4715  elrnmpt1  5105  fmptco  5887  zfrep6  5954  elabrex  5971  nfmpt2  6128  cbvmpt2x  6136  ovmpt2dxf  6185  fmpt2x  6403  opabiota  6524  riotasvd  6578  nfrecs  6621  erovlem  6986  xpf1o  7255  mapxpen  7259  wdom2d  7532  cnfcom3clem  7646  scott0  7794  cplem2  7798  infxpenc2lem2  7885  acnlem  7913  fin23lem32  8208  hsmexlem2  8291  axcc3  8302  ac6num  8343  lble  9944  nfsum1  12467  nfsum  12468  fsum  12497  fsumcvg2  12504  fsum2dlem  12537  infcvgaux1i  12619  neiptopreu  17180  xkocnv  17829  cnlnadjlem5  23557  chirred  23881  iundisjf  24012  dfimafnf  24026  cbvmptf  24051  fmptcof2  24059  iota5f  25165  nfcprod1  25220  nfcprod  25221  zprod  25247  fprod  25251  fprodser  25259  fprod2dlem  25288  itg2addnclem  26197  cover2  26347  indexa  26367  elnn0rabdioph  26795  wdom2d2  27038  fmuldfeqlem1  27621  stoweidlem8  27666  stoweidlem16  27674  stoweidlem19  27677  stoweidlem21  27679  stoweidlem22  27680  stoweidlem23  27681  stoweidlem29  27687  stoweidlem32  27690  stoweidlem35  27693  stoweidlem36  27694  stoweidlem41  27699  stoweidlem44  27702  stoweidlem45  27703  stoweidlem51  27709  stoweidlem53  27711  stoweidlem60  27718  bnj1468  28969  bnj981  29073  bnj1463  29176  cdleme31sn1  30909  cdleme32fva  30965  cdlemk36  31441
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-cleq 2423  df-clel 2426  df-nfc 2555
  Copyright terms: Public domain W3C validator