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

Theorem nfeq1 2586
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 2577 . 2  |-  F/_ x B
31, 2nfeq 2584 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1364   F/wnf 1594   F/_wnfc 2564
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-cleq 2434  df-clel 2437  df-nfc 2566
This theorem is referenced by:  euabsn  3944  disjxun  4287  reusv6OLD  4500  opabiotafun  5749  fvmptt  5786  eusvobj2  6082  ovmpt2dv2  6223  ov3  6226  dom2lem  7345  pwfseqlem2  8822  fsumf1o  13196  isummulc2  13225  fsum00  13257  isumshft  13298  iserodd  13898  yonedalem4b  15082  gsum2d2lem  16455  elptr2  19106  ovoliunnul  20949  mbfinf  21102  itg2splitlem  21185  dgrle  21670  disjabrex  25861  disjabrexf  25862  voliune  26581  volfiniune  26582  zprod  27379  fprodf1o  27388  prodss  27389  finminlem  28438  eq0rabdioph  29040  monotoddzz  29209  stoweidlem28  29748  stoweidlem48  29768  stoweidlem58  29778  oprabv  30082  bnj958  31767  bnj1491  31882  cdleme43fsv1snlem  33786  ltrniotaval  33947  cdlemksv2  34213  cdlemkuv2  34233  cdlemk36  34279  cdlemkid  34302  cdlemk19x  34309
  Copyright terms: Public domain W3C validator