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

Theorem nfeq1 2637
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 2622 . 2  |-  F/_ x B
31, 2nfeq 2633 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374   F/wnf 1594   F/_wnfc 2608
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 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-cleq 2452  df-nfc 2610
This theorem is referenced by:  euabsn  4092  disjxun  4438  reusv6OLD  4651  opabiotafun  5919  fvmptt  5956  eusvobj2  6268  oprabv  6320  ovmpt2dv2  6411  ov3  6414  dom2lem  7545  pwfseqlem2  9026  fsumf1o  13494  isummulc2  13526  fsum00  13561  isumshft  13603  iserodd  14207  yonedalem4b  15392  gsum2d2lem  16785  gsummptnn0fz  16798  gsummoncoe1  18110  elptr2  19803  ovoliunnul  21646  mbfinf  21800  itg2splitlem  21883  dgrle  22368  disjabrex  27102  disjabrexf  27103  voliune  27827  volfiniune  27828  zprod  28632  fprodf1o  28641  prodss  28642  finminlem  29700  eq0rabdioph  30301  monotoddzz  30470  stoweidlem28  31283  stoweidlem48  31303  stoweidlem58  31313  bnj958  32952  bnj1491  33067  cdleme43fsv1snlem  35091  ltrniotaval  35252  cdlemksv2  35518  cdlemkuv2  35538  cdlemk36  35584  cdlemkid  35607  cdlemk19x  35614
  Copyright terms: Public domain W3C validator