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

Theorem nfeq2 2396
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 2385 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2392 1  |-  F/ x  A  =  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1539    = wceq 1619   F/_wnfc 2372
This theorem is referenced by:  issetf  2732  eqvincf  2833  csbhypf  3044  nfpr  3584  intab  3790  nfmpt  4005  cbvmpt  4007  zfrepclf  4034  moop2  4154  eusvnf  4420  reusv2lem4  4429  reusv2  4431  elrnmpt1  4835  fmptco  5543  zfrep6  5600  elabrex  5617  nfmpt2  5768  cbvmpt2x  5776  ovmpt2dxf  5825  fmpt2x  6042  riotasvd  6233  nfrecs  6276  erovlem  6640  xpf1o  6908  mapxpen  6912  wdom2d  7178  cnfcom3clem  7292  scott0  7440  cplem2  7444  infxpenc2lem2  7531  acnlem  7559  fin23lem32  7854  hsmexlem2  7937  axcc3  7948  ac6num  7990  lble  9586  nfsum1  12040  nfsum  12041  fsum  12070  fsumcvg2  12077  fsum2dlem  12110  infcvgaux1i  12189  xkocnv  17337  cnlnadjlem5  22481  chirred  22805  svli2  24650  intopcoaconb  24706  cnegvex2  24826  rnegvex2  24827  cover2  25524  indexa  25578  elnn0rabdioph  26050  wdom2d2  26294  bnj1468  27567  bnj981  27671  bnj1463  27774  cdleme31sn1  29259  cdleme32fva  29315  cdlemk36  29791
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 1926  ax-ext 2234
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 1883  df-cleq 2246  df-clel 2249  df-nfc 2374
  Copyright terms: Public domain W3C validator