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

Theorem nfeq2 2443
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 2432 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2439 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1534    = wceq 1632   F/_wnfc 2419
This theorem is referenced by:  issetf  2806  eqvincf  2909  csbhypf  3129  nfpr  3693  intab  3908  nfmpt  4124  cbvmpt  4126  zfrepclf  4153  moop2  4277  eusvnf  4545  reusv2lem4  4554  reusv2  4556  elrnmpt1  4944  fmptco  5707  zfrep6  5764  elabrex  5781  nfmpt2  5932  cbvmpt2x  5940  ovmpt2dxf  5989  fmpt2x  6206  riotasvd  6363  nfrecs  6406  erovlem  6770  xpf1o  7039  mapxpen  7043  wdom2d  7310  cnfcom3clem  7424  scott0  7572  cplem2  7576  infxpenc2lem2  7663  acnlem  7691  fin23lem32  7986  hsmexlem2  8069  axcc3  8080  ac6num  8122  lble  9722  nfsum1  12179  nfsum  12180  fsum  12209  fsumcvg2  12216  fsum2dlem  12249  infcvgaux1i  12331  xkocnv  17521  cnlnadjlem5  22667  chirred  22991  cbvmptf  23235  fmptcof2  23244  nfcprod1  24132  nfcprod  24133  zprod  24160  fprod  24164  svli2  25587  intopcoaconb  25643  cnegvex2  25763  rnegvex2  25764  cover2  26461  indexa  26515  elnn0rabdioph  26987  wdom2d2  27231  bnj1468  29194  bnj981  29298  bnj1463  29401  cdleme31sn1  31192  cdleme32fva  31248  cdlemk36  31724
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421
  Copyright terms: Public domain W3C validator