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

Theorem nfeq1 2532
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 2523 . 2  |-  F/_ x B
31, 2nfeq 2530 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1550    = wceq 1649   F/_wnfc 2510
This theorem is referenced by:  euabsn  3819  disjxun  4151  reusv6OLD  4674  fvmptt  5759  ovmpt2dv2  6146  ov3  6149  opabiotafun  6472  eusvobj2  6518  dom2lem  7083  pwfseqlem2  8467  zsum  12439  fsumf1o  12444  isummulc2  12473  fsum00  12504  isumshft  12546  iserodd  13136  yonedalem4b  14300  gsum2d2lem  15474  elptr2  17527  ovoliunnul  19270  mbfinf  19424  itg2splitlem  19507  dgrle  20029  disjabrex  23868  disjabrexf  23869  voliune  24379  volfiniune  24380  zprod  25042  fprodf1o  25051  prodss  25052  finminlem  26012  eq0rabdioph  26526  monotoddzz  26697  stoweidlem28  27445  stoweidlem48  27465  stoweidlem58  27475  bnj958  28649  bnj1491  28764  cdleme43fsv1snlem  30534  ltrniotaval  30695  cdlemksv2  30961  cdlemkuv2  30981  cdlemk36  31027  cdlemkid  31050  cdlemk19x  31057
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2380  df-clel 2383  df-nfc 2512
  Copyright terms: Public domain W3C validator