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

Theorem nfeq2 2589
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 2578 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2585 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1554    = wceq 1653   F/_wnfc 2565
This theorem is referenced by:  issetf  2967  eqvincf  3070  csbhypf  3285  nfpr  3879  intab  4104  nfmpt  4322  cbvmpt  4324  zfrepclf  4351  moop2  4480  eusvnf  4747  reusv2lem4  4756  reusv2  4758  elrnmpt1  5148  fmptco  5930  zfrep6  5997  elabrex  6014  nfmpt2  6171  cbvmpt2x  6179  ovmpt2dxf  6228  fmpt2x  6446  opabiota  6567  riotasvd  6621  nfrecs  6664  erovlem  7029  xpf1o  7298  mapxpen  7302  wdom2d  7577  cnfcom3clem  7691  scott0  7841  cplem2  7845  infxpenc2lem2  7932  acnlem  7960  fin23lem32  8255  hsmexlem2  8338  axcc3  8349  ac6num  8390  lble  9991  nfsum1  12515  nfsum  12516  fsum  12545  fsumcvg2  12552  fsum2dlem  12585  infcvgaux1i  12667  neiptopreu  17228  xkocnv  17877  cnlnadjlem5  23605  chirred  23929  iundisjf  24060  dfimafnf  24074  cbvmptf  24099  fmptcof2  24107  iota5f  25213  nfcprod1  25267  nfcprod  25268  zprod  25294  fprod  25298  fprodser  25306  fprod2dlem  25335  nfwrecs  25564  nfwlim  25604  itg2addnclem  26294  cover2  26453  indexa  26473  elnn0rabdioph  26901  wdom2d2  27144  fmuldfeqlem1  27726  stoweidlem8  27771  stoweidlem16  27779  stoweidlem19  27782  stoweidlem21  27784  stoweidlem22  27785  stoweidlem23  27786  stoweidlem29  27792  stoweidlem32  27795  stoweidlem35  27798  stoweidlem36  27799  stoweidlem41  27804  stoweidlem44  27807  stoweidlem45  27808  stoweidlem51  27814  stoweidlem53  27816  stoweidlem60  27823  bnj1468  29315  bnj981  29419  bnj1463  29522  cdleme31sn1  31276  cdleme32fva  31332  cdlemk36  31808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-cleq 2435  df-clel 2438  df-nfc 2567
  Copyright terms: Public domain W3C validator