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

Theorem nfeq2 2534
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 2523 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2530 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1550    = wceq 1649   F/_wnfc 2510
This theorem is referenced by:  issetf  2904  eqvincf  3007  csbhypf  3229  nfpr  3798  intab  4022  nfmpt  4238  cbvmpt  4240  zfrepclf  4267  moop2  4392  eusvnf  4658  reusv2lem4  4667  reusv2  4669  elrnmpt1  5059  fmptco  5840  zfrep6  5907  elabrex  5924  nfmpt2  6081  cbvmpt2x  6089  ovmpt2dxf  6138  fmpt2x  6356  opabiota  6474  riotasvd  6528  nfrecs  6571  erovlem  6936  xpf1o  7205  mapxpen  7209  wdom2d  7481  cnfcom3clem  7595  scott0  7743  cplem2  7747  infxpenc2lem2  7834  acnlem  7862  fin23lem32  8157  hsmexlem2  8240  axcc3  8251  ac6num  8292  lble  9892  nfsum1  12411  nfsum  12412  fsum  12441  fsumcvg2  12448  fsum2dlem  12481  infcvgaux1i  12563  neiptopreu  17120  xkocnv  17767  cnlnadjlem5  23422  chirred  23746  iundisjf  23872  dfimafnf  23886  cbvmptf  23910  fmptcof2  23918  iota5f  24961  nfcprod1  25015  nfcprod  25016  zprod  25042  fprod  25046  fprodser  25054  cover2  26106  indexa  26126  elnn0rabdioph  26554  wdom2d2  26797  fmuldfeqlem1  27380  stoweidlem8  27425  stoweidlem16  27433  stoweidlem19  27436  stoweidlem21  27438  stoweidlem22  27439  stoweidlem23  27440  stoweidlem29  27446  stoweidlem32  27449  stoweidlem35  27452  stoweidlem36  27453  stoweidlem41  27458  stoweidlem44  27461  stoweidlem45  27462  stoweidlem51  27468  stoweidlem53  27470  stoweidlem60  27477  bnj1468  28555  bnj981  28659  bnj1463  28762  cdleme31sn1  30495  cdleme32fva  30551  cdlemk36  31027
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2380  df-clel 2383  df-nfc 2512
  Copyright terms: Public domain W3C validator