Theorem nfeq2 2929

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

Syntax hints:   = wceq 1631  Ⅎwnf 1856  Ⅎwnfc 2900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-tru 1634  df-ex 1853  df-nf 1858  df-cleq 2764  df-nfc 2902

This theorem is referenced by:  issetf  3360  eqvincf  3482  csbhypf  3702  nfpr  4370  intab  4642  nfmpt  4881  cbvmptf  4883  cbvmpt  4884  zfrepclf  4912  eusvnf  4993  reusv2lem4  5002  reusv2  5004  moop2  5094  elrnmpt1  5513  opabiota  6404  fmptco  6540  elabrex  6645  nfmpt2  6872  cbvmpt2x  6881  ovmpt2dxf  6934  zfrep6  7282  fmpt2x  7387  nfwrecs  7562  erovlem  7997  xpf1o  8279  mapxpen  8283  wdom2d  8642  cnfcom3clem  8767  scott0  8914  cplem2  8918  infxpenc2lem2  9044  acnlem  9072  fin23lem32  9369  hsmexlem2  9452  axcc3  9463  ac6num  9504  lble  11178  nfsum1  14629  nfsum  14630  zsum  14658  fsum  14660  fsumcvg2  14667  fsum2dlem  14710  infcvgaux1i  14797  nfcprod1  14848  nfcprod  14849  zprod  14875  fprod  14879  fprodser  14887  fprod2dlem  14918  cayleyhamilton1  20918  neiptopreu  21159  xkocnv  21839  istrkg2ld  25581  cnlnadjlem5  29271  chirred  29595  iundisjf  29741  opabdm  29762  opabrn  29763  dfimafnf  29777  fmptcof2  29798  mpt2mptxf  29818  f1od2  29840  fpwrelmap  29849  esum2dlem  30495  oms0  30700  bnj1468  31255  bnj981  31359  bnj1463  31462  iota5f  31945  nfwlim  32105  nffrecs  32116  bj-seex  33251  isbasisrelowllem1  33541  isbasisrelowllem2  33542  finxpreclem6  33571  cnfinltrel  33579  phpreu  33727  matunitlindflem2  33740  poimirlem24  33767  poimirlem25  33768  poimirlem26  33769  poimirlem27  33770  mbfposadd  33790  itg2addnclem  33794  cover2  33841  indexa  33861  riotasvd  34765  cdleme31sn1  36191  cdleme32fva  36247  cdlemk36  36723  elnn0rabdioph  37894  wdom2d2  38129  elabrexg  39729  cbvmpt22  39799  cbvmpt21  39800  fmuldfeqlem1  40333  climf  40373  climf2  40417  cncficcgt0  40620  stoweidlem8  40743  stoweidlem16  40751  stoweidlem19  40754  stoweidlem21  40756  stoweidlem22  40757  stoweidlem23  40758  stoweidlem29  40764  stoweidlem32  40767  stoweidlem35  40770  stoweidlem36  40771  stoweidlem41  40776  stoweidlem44  40779  stoweidlem45  40780  stoweidlem51  40786  stoweidlem53  40788  stoweidlem60  40795  fourierdlem80  40921  sprsymrelf  42274  cbvmpt2x2  42643  ovmpt2rdxf  42646