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

Theorem nfeq2 2432
Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq2.1  |-  F/_ x B
Assertion
Ref Expression
nfeq2  |-  F/ x  A  =  B
Distinct variable group:    x, A
Allowed substitution hint:    B( x)

Proof of Theorem nfeq2
StepHypRef Expression
1 nfcv 2421 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2428 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1532    = wceq 1624   F/_wnfc 2408
This theorem is referenced by:  issetf  2795  eqvincf  2898  csbhypf  3118  nfpr  3682  intab  3894  nfmpt  4110  cbvmpt  4112  zfrepclf  4139  moop2  4261  eusvnf  4529  reusv2lem4  4538  reusv2  4540  elrnmpt1  4928  fmptco  5653  zfrep6  5710  elabrex  5727  nfmpt2  5878  cbvmpt2x  5886  ovmpt2dxf  5935  fmpt2x  6152  riotasvd  6343  nfrecs  6386  erovlem  6750  xpf1o  7019  mapxpen  7023  wdom2d  7290  cnfcom3clem  7404  scott0  7552  cplem2  7556  infxpenc2lem2  7643  acnlem  7671  fin23lem32  7966  hsmexlem2  8049  axcc3  8060  ac6num  8102  lble  9702  nfsum1  12158  nfsum  12159  fsum  12188  fsumcvg2  12195  fsum2dlem  12228  infcvgaux1i  12310  xkocnv  17500  cnlnadjlem5  22644  chirred  22968  svli2  24884  intopcoaconb  24940  cnegvex2  25060  rnegvex2  25061  cover2  25758  indexa  25812  elnn0rabdioph  26284  wdom2d2  26528  bnj1468  28146  bnj981  28250  bnj1463  28353  cdleme31sn1  29838  cdleme32fva  29894  cdlemk36  30370
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-cleq 2278  df-clel 2281  df-nfc 2410
  Copyright terms: Public domain W3C validator