Theorem nfeq2 2921

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 2904	. 2 ⊢ Ⅎ𝑥𝐴
2		nfeq2.1	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2917	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1542  Ⅎwnf 1786  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-cleq 2725  df-nfc 2886

This theorem is referenced by:  issetf  3489  eqvincf  3638  csbhypf  3922  nfpr  4694  intab  4982  nfmpt  5255  cbvmptf  5257  cbvmptfg  5258  zfrepclf  5294  eusvnf  5390  reusv2lem4  5399  reusv2  5401  moop2  5502  elrnmpt1  5956  opabiota  6972  fvmptdf  7002  fmptco  7124  elabrex  7239  nfmpo  7488  cbvmpox  7499  ovmpodxf  7555  zfrep6  7938  fmpox  8050  nffrecs  8265  nfwrecsOLD  8299  erovlem  8804  xpf1o  9136  mapxpen  9140  wdom2d  9572  cnfcom3clem  9697  scott0  9878  cplem2  9882  infxpenc2lem2  10012  acnlem  10040  fin23lem32  10336  hsmexlem2  10419  axcc3  10430  ac6num  10471  lble  12163  nfsum1  15633  nfsum  15634  zsum  15661  fsum  15663  fsumcvg2  15670  fsum2dlem  15713  infcvgaux1i  15800  nfcprod1  15851  nfcprod  15852  zprod  15878  fprod  15882  fprodser  15890  fprod2dlem  15921  cayleyhamilton1  22386  neiptopreu  22629  xkocnv  23310  istrkg2ld  27701  cnlnadjlem5  31312  chirred  31636  iundisjf  31808  opabdm  31828  opabrn  31829  dfimafnf  31848  fmptcof2  31870  mpomptxf  31893  f1od2  31934  fpwrelmap  31946  elrspunidl  32535  fedgmullem2  32704  esum2dlem  33079  oms0  33285  bnj1468  33846  bnj981  33950  bnj1463  34055  satfv1  34343  iota5f  34682  nfwlim  34783  bj-seex  35791  isbasisrelowllem1  36225  isbasisrelowllem2  36226  exrecfnlem  36249  finxpreclem6  36266  phpreu  36461  matunitlindflem2  36474  poimirlem24  36501  poimirlem25  36502  poimirlem26  36503  poimirlem27  36504  mbfposadd  36524  itg2addnclem  36528  cover2  36572  indexa  36590  riotasvd  37815  cdleme31sn1  39241  cdleme32fva  39297  cdlemk36  39773  elnn0rabdioph  41527  wdom2d2  41760  elabrexg  43714  cbvmpo2  43772  cbvmpo1  43773  dffo3f  43863  elrnmptf  43864  disjrnmpt2  43872  fmuldfeqlem1  44285  climf  44325  climf2  44369  cncficcgt0  44591  stoweidlem8  44711  stoweidlem16  44719  stoweidlem19  44722  stoweidlem21  44724  stoweidlem22  44725  stoweidlem23  44726  stoweidlem29  44732  stoweidlem32  44735  stoweidlem35  44738  stoweidlem36  44739  stoweidlem41  44744  stoweidlem44  44747  stoweidlem45  44748  stoweidlem51  44754  stoweidlem53  44756  stoweidlem60  44763  fourierdlem80  44889  sprsymrelf  46150  cbvmpox2  46965  ovmpordxf  46968  1arymaptfo  47283  2arymaptfo  47294