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

Theorem nfeq2 2618
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 2603 . 2  |-  F/_ x A
2 nfeq2.1 . 2  |-  F/_ x B
31, 2nfeq 2614 1  |-  F/ x  A  =  B
Colors of variables: wff setvar class
Syntax hints:    = wceq 1455   F/wnf 1678   F/_wnfc 2590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-cleq 2455  df-nfc 2592
This theorem is referenced by:  issetf  3062  eqvincf  3179  csbhypf  3394  nfpr  4031  intab  4279  nfmpt  4505  cbvmptf  4507  cbvmpt  4508  zfrepclf  4535  eusvnf  4612  reusv2lem4  4621  reusv2  4623  moop2  4710  elrnmpt1  5102  opabiota  5951  fmptco  6080  elabrex  6173  nfmpt2  6387  cbvmpt2x  6396  ovmpt2dxf  6449  zfrep6  6788  fmpt2x  6886  nfwrecs  7056  erovlem  7485  xpf1o  7760  mapxpen  7764  wdom2d  8121  cnfcom3clem  8236  scott0  8383  cplem2  8387  infxpenc2lem2  8477  acnlem  8505  fin23lem32  8800  hsmexlem2  8883  axcc3  8894  ac6num  8935  lble  10586  nfsum1  13805  nfsum  13806  zsum  13833  fsum  13835  fsumcvg2  13842  fsum2dlem  13880  infcvgaux1i  13964  nfcprod1  14013  nfcprod  14014  zprod  14040  fprod  14044  fprodser  14052  fprod2dlem  14083  cayleyhamilton1  19965  neiptopreu  20198  xkocnv  20878  istrkg2ld  24557  cnlnadjlem5  27773  chirred  28097  iundisjf  28248  opabdm  28268  opabrn  28269  dfimafnf  28282  fmptcof2  28308  mpt2mptxf  28329  f1od2  28358  fpwrelmap  28367  esum2dlem  28962  oms0  29174  bnj1468  29706  bnj981  29810  bnj1463  29913  iota5f  30406  nfwlim  30554  bj-seex  31571  isbasisrelowllem1  31803  isbasisrelowllem2  31804  finxpreclem6  31833  phpreu  31974  poimirlem24  32009  poimirlem25  32010  poimirlem26  32011  poimirlem27  32012  mbfposadd  32033  itg2addnclem  32038  cover2  32085  indexa  32105  riotasvd  32573  cdleme31sn1  33993  cdleme32fva  34049  cdlemk36  34525  elnn0rabdioph  35691  wdom2d2  35935  elabrexg  37409  fmuldfeqlem1  37698  climf  37740  cncficcgt0  37804  stoweidlem8  37906  stoweidlem16  37914  stoweidlem19  37917  stoweidlem21  37919  stoweidlem22  37920  stoweidlem23  37921  stoweidlem29  37927  stoweidlem29OLD  37928  stoweidlem32  37931  stoweidlem35  37934  stoweidlem36  37935  stoweidlem41  37940  stoweidlem44  37943  stoweidlem45  37944  stoweidlem51  37950  stoweidlem53  37952  stoweidlem60  37959  fourierdlem80  38088  cbvmpt2x2  40390  ovmpt2rdxf  40393
  Copyright terms: Public domain W3C validator