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

Theorem nfeq2 2633
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 2616 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2627 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398   F/wnf 1621   F/_wnfc 2602
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-cleq 2446  df-nfc 2604
This theorem is referenced by:  issetf  3111  eqvincf  3224  csbhypf  3439  nfpr  4063  intab  4302  nfmpt  4527  cbvmpt  4529  zfrepclf  4556  eusvnf  4632  reusv2lem4  4641  reusv2  4643  moop2  4731  elrnmpt1  5240  opabiota  5911  fmptco  6040  elabrex  6130  nfmpt2  6339  cbvmpt2x  6348  ovmpt2dxf  6401  zfrep6  6741  fmpt2x  6839  nfrecs  7036  erovlem  7399  xpf1o  7672  mapxpen  7676  wdom2d  7998  cnfcom3clem  8140  cnfcom3clemOLD  8148  scott0  8295  cplem2  8299  infxpenc2lem2  8388  infxpenc2lem2OLD  8392  acnlem  8420  fin23lem32  8715  hsmexlem2  8798  axcc3  8809  ac6num  8850  lble  10490  nfsum1  13594  nfsum  13595  zsum  13622  fsum  13624  fsumcvg2  13631  fsum2dlem  13667  infcvgaux1i  13750  nfcprod1  13799  nfcprod  13800  zprod  13826  fprod  13830  fprodser  13838  fprod2dlem  13866  cayleyhamilton1  19560  neiptopreu  19801  xkocnv  20481  istrkg2ld  24056  cnlnadjlem5  27188  chirred  27512  iundisjf  27659  opabdm  27679  opabrn  27680  dfimafnf  27694  cbvmptf  27715  fmptcof2  27724  mpt2mptxf  27746  f1od2  27778  fpwrelmap  27787  esum2dlem  28321  iota5f  29343  nfwrecs  29578  nfwlim  29618  mbfposadd  30302  itg2addnclem  30306  cover2  30444  indexa  30464  elnn0rabdioph  30976  wdom2d2  31216  elabrexg  31670  fmuldfeqlem1  31815  climf  31867  cncficcgt0  31930  stoweidlem8  32029  stoweidlem16  32037  stoweidlem19  32040  stoweidlem21  32042  stoweidlem22  32043  stoweidlem23  32044  stoweidlem29  32050  stoweidlem32  32053  stoweidlem35  32056  stoweidlem36  32057  stoweidlem41  32062  stoweidlem44  32065  stoweidlem45  32066  stoweidlem51  32072  stoweidlem53  32074  stoweidlem60  32081  fourierdlem80  32208  cbvmpt2x2  33179  ovmpt2rdxf  33182  bnj1468  34305  bnj981  34409  bnj1463  34512  bj-seex  34892  riotasvd  35084  cdleme31sn1  36504  cdleme32fva  36560  cdlemk36  37036
  Copyright terms: Public domain W3C validator