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

Theorem nfeq2 2602
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 2585 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2596 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1438   F/wnf 1662   F/_wnfc 2571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-10 1892  ax-11 1897  ax-12 1910  ax-ext 2402
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1659  df-nf 1663  df-cleq 2415  df-nfc 2573
This theorem is referenced by:  issetf  3090  eqvincf  3205  csbhypf  3420  nfpr  4053  intab  4292  nfmpt  4518  cbvmptf  4520  cbvmpt  4521  zfrepclf  4548  eusvnf  4625  reusv2lem4  4634  reusv2  4636  moop2  4721  elrnmpt1  5108  opabiota  5950  fmptco  6077  elabrex  6169  nfmpt2  6380  cbvmpt2x  6389  ovmpt2dxf  6442  zfrep6  6781  fmpt2x  6879  nfwrecs  7047  erovlem  7476  xpf1o  7749  mapxpen  7753  wdom2d  8110  cnfcom3clem  8224  scott0  8371  cplem2  8375  infxpenc2lem2  8464  acnlem  8492  fin23lem32  8787  hsmexlem2  8870  axcc3  8881  ac6num  8922  lble  10571  nfsum1  13761  nfsum  13762  zsum  13789  fsum  13791  fsumcvg2  13798  fsum2dlem  13836  infcvgaux1i  13920  nfcprod1  13969  nfcprod  13970  zprod  13996  fprod  14000  fprodser  14008  fprod2dlem  14039  cayleyhamilton1  19920  neiptopreu  20153  xkocnv  20833  istrkg2ld  24512  cnlnadjlem5  27728  chirred  28052  iundisjf  28207  opabdm  28227  opabrn  28228  dfimafnf  28241  fmptcof2  28267  mpt2mptxf  28288  f1od2  28321  fpwrelmap  28330  esum2dlem  28927  oms0  29139  bnj1468  29671  bnj981  29775  bnj1463  29878  iota5f  30371  nfwlim  30518  bj-seex  31501  isbasisrelowllem1  31728  isbasisrelowllem2  31729  finxpreclem6  31758  phpreu  31899  poimirlem24  31934  poimirlem25  31935  poimirlem26  31936  poimirlem27  31937  mbfposadd  31958  itg2addnclem  31963  cover2  32010  indexa  32030  riotasvd  32503  cdleme31sn1  33923  cdleme32fva  33979  cdlemk36  34455  elnn0rabdioph  35621  wdom2d2  35866  elabrexg  37349  fmuldfeqlem1  37606  climf  37648  cncficcgt0  37712  stoweidlem8  37814  stoweidlem16  37822  stoweidlem19  37825  stoweidlem21  37827  stoweidlem22  37828  stoweidlem23  37829  stoweidlem29  37835  stoweidlem29OLD  37836  stoweidlem32  37839  stoweidlem35  37842  stoweidlem36  37843  stoweidlem41  37848  stoweidlem44  37851  stoweidlem45  37852  stoweidlem51  37858  stoweidlem53  37860  stoweidlem60  37867  fourierdlem80  37996  cbvmpt2x2  39736  ovmpt2rdxf  39739
  Copyright terms: Public domain W3C validator