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

Theorem nfeq2 2403
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 2392 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2399 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1539    = wceq 1619   F/_wnfc 2379
This theorem is referenced by:  issetf  2762  eqvincf  2864  csbhypf  3077  nfpr  3640  intab  3852  nfmpt  4068  cbvmpt  4070  zfrepclf  4097  moop2  4219  eusvnf  4487  reusv2lem4  4496  reusv2  4498  elrnmpt1  4902  fmptco  5611  zfrep6  5668  elabrex  5685  nfmpt2  5836  cbvmpt2x  5844  ovmpt2dxf  5893  fmpt2x  6110  riotasvd  6301  nfrecs  6344  erovlem  6708  xpf1o  6977  mapxpen  6981  wdom2d  7248  cnfcom3clem  7362  scott0  7510  cplem2  7514  infxpenc2lem2  7601  acnlem  7629  fin23lem32  7924  hsmexlem2  8007  axcc3  8018  ac6num  8060  lble  9660  nfsum1  12114  nfsum  12115  fsum  12144  fsumcvg2  12151  fsum2dlem  12184  infcvgaux1i  12263  xkocnv  17453  cnlnadjlem5  22597  chirred  22921  svli2  24837  intopcoaconb  24893  cnegvex2  25013  rnegvex2  25014  cover2  25711  indexa  25765  elnn0rabdioph  26237  wdom2d2  26481  bnj1468  27911  bnj981  28015  bnj1463  28118  cdleme31sn1  29721  cdleme32fva  29777  cdlemk36  30253
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-cleq 2249  df-clel 2252  df-nfc 2381
  Copyright terms: Public domain W3C validator