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

Theorem nfeq1 2620
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 2605 . 2  |-  F/_ x B
31, 2nfeq 2616 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383   F/wnf 1603   F/_wnfc 2591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-cleq 2435  df-nfc 2593
This theorem is referenced by:  euabsn  4087  disjxun  4435  reusv6OLD  4648  opabiotafun  5919  fvmptt  5956  eusvobj2  6274  oprabv  6330  ovmpt2dv2  6421  ov3  6424  dom2lem  7557  pwfseqlem2  9040  fsumf1o  13527  isummulc2  13559  fsum00  13594  isumshft  13633  zprod  13726  fprodf1o  13735  prodss  13736  iserodd  14341  yonedalem4b  15524  gsum2d2lem  16980  gsummptnn0fz  16993  gsummoncoe1  18325  elptr2  20053  ovoliunnul  21896  mbfinf  22050  itg2splitlem  22133  dgrle  22618  disjabrex  27421  disjabrexf  27422  disjunsn  27431  voliune  28179  volfiniune  28180  finminlem  30112  eq0rabdioph  30686  monotoddzz  30855  cncfiooicclem1  31650  stoweidlem28  31764  stoweidlem48  31784  stoweidlem58  31794  bnj958  33866  bnj1491  33981  cdleme43fsv1snlem  36021  ltrniotaval  36182  cdlemksv2  36448  cdlemkuv2  36468  cdlemk36  36514  cdlemkid  36537  cdlemk19x  36544
  Copyright terms: Public domain W3C validator