Theorem nfeq2 2780

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

Step	Hyp	Ref	Expression
1		nfcv 2764	. 2 |- F/_ x A
2		nfeq2.1	. 2 |- F/_ x B
3	1, 2	nfeq 2776	1 |- F/ x A = B

Syntax hints:   = wceq 1483   F/wnf 1708   F/_wnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-cleq 2615  df-nfc 2753

This theorem is referenced by:  issetf  3208  eqvincf  3331  csbhypf  3552  nfpr  4232  intab  4507  nfmpt  4746  cbvmptf  4748  cbvmpt  4749  zfrepclf  4777  eusvnf  4861  reusv2lem4  4872  reusv2  4874  moop2  4966  elrnmpt1  5374  opabiota  6261  fmptco  6396  elabrex  6501  nfmpt2  6724  cbvmpt2x  6733  ovmpt2dxf  6786  zfrep6  7134  fmpt2x  7236  nfwrecs  7409  erovlem  7843  xpf1o  8122  mapxpen  8126  wdom2d  8485  cnfcom3clem  8602  scott0  8749  cplem2  8753  infxpenc2lem2  8843  acnlem  8871  fin23lem32  9166  hsmexlem2  9249  axcc3  9260  ac6num  9301  lble  10975  nfsum1  14420  nfsum  14421  zsum  14449  fsum  14451  fsumcvg2  14458  fsum2dlem  14501  infcvgaux1i  14589  nfcprod1  14640  nfcprod  14641  zprod  14667  fprod  14671  fprodser  14679  fprod2dlem  14710  cayleyhamilton1  20697  neiptopreu  20937  xkocnv  21617  istrkg2ld  25359  cnlnadjlem5  28930  chirred  29254  iundisjf  29402  opabdm  29423  opabrn  29424  dfimafnf  29436  fmptcof2  29457  mpt2mptxf  29477  f1od2  29499  fpwrelmap  29508  esum2dlem  30154  oms0  30359  bnj1468  30916  bnj981  31020  bnj1463  31123  iota5f  31606  nfwlim  31768  bj-seex  32919  isbasisrelowllem1  33203  isbasisrelowllem2  33204  finxpreclem6  33233  phpreu  33393  matunitlindflem2  33406  poimirlem24  33433  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  mbfposadd  33457  itg2addnclem  33461  cover2  33508  indexa  33528  riotasvd  34242  cdleme31sn1  35669  cdleme32fva  35725  cdlemk36  36201  elnn0rabdioph  37367  wdom2d2  37602  elabrexg  39206  cbvmpt22  39277  cbvmpt21  39278  fmuldfeqlem1  39814  climf  39854  climf2  39898  cncficcgt0  40101  stoweidlem8  40225  stoweidlem16  40233  stoweidlem19  40236  stoweidlem21  40238  stoweidlem22  40239  stoweidlem23  40240  stoweidlem29  40246  stoweidlem32  40249  stoweidlem35  40252  stoweidlem36  40253  stoweidlem41  40258  stoweidlem44  40261  stoweidlem45  40262  stoweidlem51  40268  stoweidlem53  40270  stoweidlem60  40277  fourierdlem80  40403  sprsymrelf  41745  cbvmpt2x2  42114  ovmpt2rdxf  42117