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

Theorem nfeq1 2428
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 2419 . 2  |-  F/_ x B
31, 2nfeq 2426 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1531    = wceq 1623   F/_wnfc 2406
This theorem is referenced by:  euabsn  3699  disjxun  4021  reusv6OLD  4545  fvmptt  5615  ovmpt2dv2  5981  ov3  5984  opabiotafun  6291  eusvobj2  6337  dom2lem  6901  pwfseqlem2  8281  zsum  12191  fsumf1o  12196  isummulc2  12225  fsum00  12256  isumshft  12298  iserodd  12888  yonedalem4b  14050  gsum2d2lem  15224  elptr2  17269  ovoliunnul  18866  mbfinf  19020  itg2splitlem  19103  dgrle  19625  nfprod1  25310  nfprod  25311  finminlem  26231  eq0rabdioph  26856  monotoddzz  27028  bnj958  28972  bnj1491  29087  cdleme43fsv1snlem  30609  ltrniotaval  30770  cdlemksv2  31036  cdlemkuv2  31056  cdlemk36  31102  cdlemkid  31125  cdlemk19x  31132
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408
  Copyright terms: Public domain W3C validator