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

Theorem nfeq1 2591
Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq1.1  |-  F/_ x A
Assertion
Ref Expression
nfeq1  |-  F/ x  A  =  B
Distinct variable group:    x, B
Allowed substitution hint:    A( x)

Proof of Theorem nfeq1
StepHypRef Expression
1 nfeq1.1 . 2  |-  F/_ x A
2 nfcv 2582 . 2  |-  F/_ x B
31, 2nfeq 2589 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369   F/wnf 1589   F/_wnfc 2569
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 2423
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 2436  df-clel 2439  df-nfc 2571
This theorem is referenced by:  euabsn  3950  disjxun  4293  reusv6OLD  4506  opabiotafun  5755  fvmptt  5792  eusvobj2  6087  ovmpt2dv2  6227  ov3  6230  dom2lem  7352  pwfseqlem2  8829  fsumf1o  13203  isummulc2  13232  fsum00  13264  isumshft  13305  iserodd  13905  yonedalem4b  15089  gsum2d2lem  16468  elptr2  19150  ovoliunnul  20993  mbfinf  21146  itg2splitlem  21229  dgrle  21714  disjabrex  25929  disjabrexf  25930  voliune  26648  volfiniune  26649  zprod  27453  fprodf1o  27462  prodss  27463  finminlem  28516  eq0rabdioph  29118  monotoddzz  29287  stoweidlem28  29826  stoweidlem48  29846  stoweidlem58  29856  oprabv  30160  gsummptnn0fz  30809  gsummoncoe1  30846  bnj958  31936  bnj1491  32051  cdleme43fsv1snlem  34067  ltrniotaval  34228  cdlemksv2  34494  cdlemkuv2  34514  cdlemk36  34560  cdlemkid  34583  cdlemk19x  34590
  Copyright terms: Public domain W3C validator