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

Theorem nfeq2 2605
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 2589 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2599 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   F/wnf 1589   F/_wnfc 2575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-cleq 2436  df-nfc 2577
This theorem is referenced by:  issetf  2998  eqvincf  3108  csbhypf  3328  nfpr  3944  intab  4179  nfmpt  4401  cbvmpt  4403  zfrepclf  4430  eusvnf  4508  reusv2lem4  4517  reusv2  4519  moop2  4607  elrnmpt1  5109  opabiota  5775  fmptco  5897  elabrex  5981  nfmpt2  6176  cbvmpt2x  6185  ovmpt2dxf  6237  zfrep6  6566  fmpt2x  6661  nfrecs  6855  erovlem  7217  xpf1o  7494  mapxpen  7498  wdom2d  7816  cnfcom3clem  7959  cnfcom3clemOLD  7967  scott0  8114  cplem2  8118  infxpenc2lem2  8207  infxpenc2lem2OLD  8211  acnlem  8239  fin23lem32  8534  hsmexlem2  8617  axcc3  8628  ac6num  8669  lble  10303  nfsum1  13188  nfsum  13189  zsum  13216  fsum  13218  fsumcvg2  13225  fsum2dlem  13258  infcvgaux1i  13340  neiptopreu  18759  xkocnv  19409  cnlnadjlem5  25497  chirred  25821  iundisjf  25953  dfimafnf  25972  cbvmptf  25993  fmptcof2  26001  iota5f  27403  nfcprod1  27445  nfcprod  27446  zprod  27472  fprod  27476  fprodser  27484  fprod2dlem  27513  nfwrecs  27741  nfwlim  27781  mbfposadd  28465  itg2addnclem  28469  cover2  28633  indexa  28653  elnn0rabdioph  29167  wdom2d2  29410  fmuldfeqlem1  29789  stoweidlem8  29829  stoweidlem16  29837  stoweidlem19  29840  stoweidlem21  29842  stoweidlem22  29843  stoweidlem23  29844  stoweidlem29  29850  stoweidlem32  29853  stoweidlem35  29856  stoweidlem36  29857  stoweidlem41  29862  stoweidlem44  29865  stoweidlem45  29866  stoweidlem51  29872  stoweidlem53  29874  stoweidlem60  29881  cbvmpt2x2  30753  ovmpt2rdxf  30756  bnj1468  31935  bnj981  32039  bnj1463  32142  bj-seex  32522  riotasvd  32703  cdleme31sn1  34121  cdleme32fva  34177  cdlemk36  34653
  Copyright terms: Public domain W3C validator