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

Theorem nfeq2 2646
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 2629 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2640 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379   F/wnf 1599   F/_wnfc 2615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-cleq 2459  df-nfc 2617
This theorem is referenced by:  issetf  3118  eqvincf  3231  csbhypf  3454  nfpr  4074  intab  4312  nfmpt  4535  cbvmpt  4537  zfrepclf  4564  eusvnf  4642  reusv2lem4  4651  reusv2  4653  moop2  4742  elrnmpt1  5251  opabiota  5931  fmptco  6055  elabrex  6144  nfmpt2  6351  cbvmpt2x  6360  ovmpt2dxf  6413  zfrep6  6753  fmpt2x  6851  nfrecs  7045  erovlem  7408  xpf1o  7680  mapxpen  7684  wdom2d  8007  cnfcom3clem  8150  cnfcom3clemOLD  8158  scott0  8305  cplem2  8309  infxpenc2lem2  8398  infxpenc2lem2OLD  8402  acnlem  8430  fin23lem32  8725  hsmexlem2  8808  axcc3  8819  ac6num  8860  lble  10496  nfsum1  13478  nfsum  13479  zsum  13506  fsum  13508  fsumcvg2  13515  fsum2dlem  13551  infcvgaux1i  13634  cayleyhamilton1  19200  neiptopreu  19440  xkocnv  20142  cnlnadjlem5  26763  chirred  27087  iundisjf  27218  dfimafnf  27243  cbvmptf  27263  fmptcof2  27271  iota5f  28853  nfcprod1  28895  nfcprod  28896  zprod  28922  fprod  28926  fprodser  28934  fprod2dlem  28963  nfwrecs  29191  nfwlim  29231  mbfposadd  29915  itg2addnclem  29919  cover2  30034  indexa  30054  elnn0rabdioph  30567  wdom2d2  30808  elabrexg  31239  fmuldfeqlem1  31359  stoweidlem8  31535  stoweidlem16  31543  stoweidlem19  31546  stoweidlem21  31548  stoweidlem22  31549  stoweidlem23  31550  stoweidlem29  31556  stoweidlem32  31559  stoweidlem35  31562  stoweidlem36  31563  stoweidlem41  31568  stoweidlem44  31571  stoweidlem45  31572  stoweidlem51  31578  stoweidlem53  31580  stoweidlem60  31587  cbvmpt2x2  32220  ovmpt2rdxf  32223  bnj1468  33200  bnj981  33304  bnj1463  33407  bj-seex  33789  riotasvd  33976  cdleme31sn1  35394  cdleme32fva  35450  cdlemk36  35926
  Copyright terms: Public domain W3C validator