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

Theorem nfeq2 2608
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 2591 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2602 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   F/wnf 1663   F/_wnfc 2577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-cleq 2421  df-nfc 2579
This theorem is referenced by:  issetf  3092  eqvincf  3205  csbhypf  3420  nfpr  4050  intab  4289  nfmpt  4514  cbvmptf  4516  cbvmpt  4517  zfrepclf  4544  eusvnf  4620  reusv2lem4  4629  reusv2  4631  moop2  4716  elrnmpt1  5103  opabiota  5944  fmptco  6071  elabrex  6163  nfmpt2  6374  cbvmpt2x  6383  ovmpt2dxf  6436  zfrep6  6775  fmpt2x  6873  nfwrecs  7038  erovlem  7467  xpf1o  7740  mapxpen  7744  wdom2d  8095  cnfcom3clem  8209  scott0  8356  cplem2  8360  infxpenc2lem2  8449  acnlem  8477  fin23lem32  8772  hsmexlem2  8855  axcc3  8866  ac6num  8907  lble  10558  nfsum1  13734  nfsum  13735  zsum  13762  fsum  13764  fsumcvg2  13771  fsum2dlem  13809  infcvgaux1i  13893  nfcprod1  13942  nfcprod  13943  zprod  13969  fprod  13973  fprodser  13981  fprod2dlem  14012  cayleyhamilton1  19847  neiptopreu  20080  xkocnv  20760  istrkg2ld  24371  cnlnadjlem5  27559  chirred  27883  iundisjf  28038  opabdm  28058  opabrn  28059  dfimafnf  28073  fmptcof2  28099  mpt2mptxf  28120  f1od2  28152  fpwrelmap  28161  esum2dlem  28752  bnj1468  29445  bnj981  29549  bnj1463  29652  iota5f  30145  nfwlim  30292  bj-seex  31276  isbasisrelowllem1  31492  isbasisrelowllem2  31493  phpreu  31633  poimirlem24  31668  poimirlem25  31669  poimirlem26  31670  poimirlem27  31671  mbfposadd  31692  itg2addnclem  31697  cover2  31744  indexa  31764  riotasvd  32237  cdleme31sn1  33657  cdleme32fva  33713  cdlemk36  34189  elnn0rabdioph  35355  wdom2d2  35596  elabrexg  37010  fmuldfeqlem1  37232  climf  37274  cncficcgt0  37338  stoweidlem8  37437  stoweidlem16  37445  stoweidlem19  37448  stoweidlem21  37450  stoweidlem22  37451  stoweidlem23  37452  stoweidlem29  37458  stoweidlem29OLD  37459  stoweidlem32  37462  stoweidlem35  37465  stoweidlem36  37466  stoweidlem41  37471  stoweidlem44  37474  stoweidlem45  37475  stoweidlem51  37481  stoweidlem53  37483  stoweidlem60  37490  fourierdlem80  37618  cbvmpt2x2  38886  ovmpt2rdxf  38889
  Copyright terms: Public domain W3C validator