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  2745  eqvincf  2847  csbhypf  3058  nfpr  3621  intab  3833  nfmpt  4048  cbvmpt  4050  zfrepclf  4077  moop2  4198  eusvnf  4466  reusv2lem4  4475  reusv2  4477  elrnmpt1  4881  fmptco  5590  zfrep6  5647  elabrex  5664  nfmpt2  5815  cbvmpt2x  5823  ovmpt2dxf  5872  fmpt2x  6089  riotasvd  6280  nfrecs  6323  erovlem  6687  xpf1o  6956  mapxpen  6960  wdom2d  7227  cnfcom3clem  7341  scott0  7489  cplem2  7493  infxpenc2lem2  7580  acnlem  7608  fin23lem32  7903  hsmexlem2  7986  axcc3  7997  ac6num  8039  lble  9639  nfsum1  12093  nfsum  12094  fsum  12123  fsumcvg2  12130  fsum2dlem  12163  infcvgaux1i  12242  xkocnv  17432  cnlnadjlem5  22576  chirred  22900  svli2  24816  intopcoaconb  24872  cnegvex2  24992  rnegvex2  24993  cover2  25690  indexa  25744  elnn0rabdioph  26216  wdom2d2  26460  bnj1468  27890  bnj981  27994  bnj1463  28097  cdleme31sn1  29700  cdleme32fva  29756  cdlemk36  30232
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