Theorem nfeq2 2917

Description: Hypothesis builder for equality, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)

Hypothesis

Ref	Expression
nfeq2.1	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfeq2	⊢ Ⅎ𝑥 𝐴 = 𝐵

Distinct variable group:   𝑥,𝐴

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfeq2

Step	Hyp	Ref	Expression
1		nfcv 2899	. 2 ⊢ Ⅎ𝑥𝐴
2		nfeq2.1	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2913	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1534  Ⅎwnf 1778  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-nf 1779  df-cleq 2720  df-nfc 2881

This theorem is referenced by:  eqvincf  3636  csbhypf  3921  nfpr  4695  intab  4981  nfmpt  5255  cbvmptf  5257  cbvmptfg  5258  zfrepclf  5294  eusvnf  5392  reusv2lem4  5401  reusv2  5403  moop2  5504  elrnmpt1  5960  opabiota  6981  fvmptdf  7011  dffo3f  7116  fmptco  7138  elabrex  7252  elabrexg  7253  nfmpo  7502  cbvmpox  7513  ovmpodxf  7571  zfrep6  7958  fmpox  8071  nffrecs  8289  nfwrecsOLD  8323  erovlem  8832  xpf1o  9164  mapxpen  9168  wdom2d  9604  cnfcom3clem  9729  scott0  9910  cplem2  9914  infxpenc2lem2  10044  acnlem  10072  fin23lem32  10368  hsmexlem2  10451  axcc3  10462  ac6num  10503  lble  12197  nfsum1  15669  nfsum  15670  zsum  15697  fsum  15699  fsumcvg2  15706  fsum2dlem  15749  infcvgaux1i  15836  nfcprod1  15887  nfcprod  15888  zprod  15914  fprod  15918  fprodser  15926  fprod2dlem  15957  cayleyhamilton1  22807  neiptopreu  23050  xkocnv  23731  istrkg2ld  28277  cnlnadjlem5  31894  chirred  32218  iundisjf  32392  opabdm  32414  opabrn  32415  dfimafnf  32434  fmptcof2  32456  mpomptxf  32477  f1od2  32516  fpwrelmap  32528  elrspunidl  33157  fedgmullem2  33328  esum2dlem  33711  oms0  33917  bnj1468  34477  bnj981  34581  bnj1463  34686  satfv1  34973  iota5f  35318  nfwlim  35418  bj-seex  36400  isbasisrelowllem1  36834  isbasisrelowllem2  36835  exrecfnlem  36858  finxpreclem6  36875  phpreu  37077  matunitlindflem2  37090  poimirlem24  37117  poimirlem25  37118  poimirlem26  37119  poimirlem27  37120  mbfposadd  37140  itg2addnclem  37144  cover2  37188  indexa  37206  riotasvd  38428  cdleme31sn1  39854  cdleme32fva  39910  cdlemk36  40386  elnn0rabdioph  42223  wdom2d2  42456  cbvmpo2  44463  cbvmpo1  44464  elrnmptf  44554  disjrnmpt2  44561  fmuldfeqlem1  44970  climf  45010  climf2  45054  cncficcgt0  45276  stoweidlem8  45396  stoweidlem16  45404  stoweidlem19  45407  stoweidlem21  45409  stoweidlem22  45410  stoweidlem23  45411  stoweidlem29  45417  stoweidlem32  45420  stoweidlem35  45423  stoweidlem36  45424  stoweidlem41  45429  stoweidlem44  45432  stoweidlem45  45433  stoweidlem51  45439  stoweidlem53  45441  stoweidlem60  45448  fourierdlem80  45574  sprsymrelf  46835  cbvmpox2  47399  ovmpordxf  47402  1arymaptfo  47716  2arymaptfo  47727

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »