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

Theorem nfeq2 2584
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 2573 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2580 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   F/wnf 1589   F/_wnfc 2560
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-13 1943  ax-ext 2418
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-cleq 2430  df-clel 2433  df-nfc 2562
This theorem is referenced by:  issetf  2971  eqvincf  3080  csbhypf  3300  nfpr  3916  intab  4151  nfmpt  4373  cbvmpt  4375  zfrepclf  4402  eusvnf  4480  reusv2lem4  4489  reusv2  4491  moop2  4579  elrnmpt1  5080  opabiota  5747  fmptco  5869  elabrex  5953  nfmpt2  6150  cbvmpt2x  6159  ovmpt2dxf  6211  zfrep6  6540  fmpt2x  6635  nfrecs  6826  erovlem  7188  xpf1o  7465  mapxpen  7469  wdom2d  7787  cnfcom3clem  7930  cnfcom3clemOLD  7938  scott0  8085  cplem2  8089  infxpenc2lem2  8178  infxpenc2lem2OLD  8182  acnlem  8210  fin23lem32  8505  hsmexlem2  8588  axcc3  8599  ac6num  8640  lble  10274  nfsum1  13159  nfsum  13160  zsum  13187  fsum  13189  fsumcvg2  13196  fsum2dlem  13229  infcvgaux1i  13311  neiptopreu  18706  xkocnv  19356  cnlnadjlem5  25420  chirred  25744  iundisjf  25876  dfimafnf  25895  cbvmptf  25916  fmptcof2  25924  iota5f  27328  nfcprod1  27370  nfcprod  27371  zprod  27397  fprod  27401  fprodser  27409  fprod2dlem  27438  nfwrecs  27666  nfwlim  27706  mbfposadd  28382  itg2addnclem  28386  cover2  28550  indexa  28570  elnn0rabdioph  29084  wdom2d2  29327  fmuldfeqlem1  29706  stoweidlem8  29746  stoweidlem16  29754  stoweidlem19  29757  stoweidlem21  29759  stoweidlem22  29760  stoweidlem23  29761  stoweidlem29  29767  stoweidlem32  29770  stoweidlem35  29773  stoweidlem36  29774  stoweidlem41  29779  stoweidlem44  29782  stoweidlem45  29783  stoweidlem51  29789  stoweidlem53  29791  stoweidlem60  29798  cbvmpt2x2  30668  ovmpt2rdxf  30671  bnj1468  31696  bnj981  31800  bnj1463  31903  bj-seex  32189  riotasvd  32358  cdleme31sn1  33776  cdleme32fva  33832  cdlemk36  34308
  Copyright terms: Public domain W3C validator