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

Theorem nfeq1 2599
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 2584 . 2  |-  F/_ x B
31, 2nfeq 2595 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437   F/wnf 1663   F/_wnfc 2570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-cleq 2414  df-nfc 2572
This theorem is referenced by:  euabsn  4069  invdisjrab  4410  disjxun  4418  opabiotafun  5938  fvmptt  5977  eusvobj2  6294  oprabv  6349  ovmpt2dv2  6440  ov3  6443  dom2lem  7612  pwfseqlem2  9084  fsumf1o  13774  isummulc2  13808  fsum00  13843  isumshft  13882  zprod  13976  fprodf1o  13985  prodss  13986  iserodd  14770  yonedalem4b  16146  gsum2d2lem  17590  gsummptnn0fz  17600  gsummoncoe1  18883  elptr2  20573  ovoliunnul  22444  mbfinf  22605  mbfinfOLD  22606  itg2splitlem  22690  dgrle  23181  disjabrex  28179  disjabrexf  28180  disjunsn  28191  voliune  29045  volfiniune  29046  bnj958  29744  bnj1491  29859  finminlem  30964  poimirlem23  31874  poimirlem28  31879  cdleme43fsv1snlem  33903  ltrniotaval  34064  cdlemksv2  34330  cdlemkuv2  34350  cdlemk36  34396  cdlemkid  34419  cdlemk19x  34426  eq0rabdioph  35535  monotoddzz  35708  cncfiooicclem1  37588  stoweidlem28  37705  stoweidlem48  37726  stoweidlem58  37736  etransclem32  37948  iunopeqop  38704
  Copyright terms: Public domain W3C validator