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

Theorem nfeq1 2631
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 2616 . 2  |-  F/_ x B
31, 2nfeq 2627 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398   F/wnf 1621   F/_wnfc 2602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-cleq 2446  df-nfc 2604
This theorem is referenced by:  euabsn  4088  invdisjrab  4429  disjxun  4437  reusv6OLD  4648  opabiotafun  5909  fvmptt  5947  eusvobj2  6263  oprabv  6318  ovmpt2dv2  6409  ov3  6412  dom2lem  7548  pwfseqlem2  9026  fsumf1o  13630  isummulc2  13662  fsum00  13697  isumshft  13736  zprod  13829  fprodf1o  13838  prodss  13839  iserodd  14446  yonedalem4b  15747  gsum2d2lem  17200  gsummptnn0fz  17212  gsummoncoe1  18544  elptr2  20244  ovoliunnul  22087  mbfinf  22241  itg2splitlem  22324  dgrle  22809  disjabrex  27656  disjabrexf  27657  disjunsn  27667  voliune  28441  volfiniune  28442  finminlem  30379  eq0rabdioph  30952  monotoddzz  31121  cncfiooicclem1  31938  stoweidlem28  32052  stoweidlem48  32072  stoweidlem58  32082  etransclem32  32291  bnj958  34418  bnj1491  34533  cdleme43fsv1snlem  36562  ltrniotaval  36723  cdlemksv2  36989  cdlemkuv2  37009  cdlemk36  37055  cdlemkid  37078  cdlemk19x  37085
  Copyright terms: Public domain W3C validator