Theorem nfeq 2980

Description: Hypothesis builder for equality. (Contributed by NM, 21-Jun-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 16-Nov-2019.)

Hypotheses

Ref	Expression
nfnfc.1	⊢ Ⅎ𝑥𝐴
nfeq.2	⊢ Ⅎ𝑥𝐵

Assertion

Ref	Expression
nfeq	⊢ Ⅎ𝑥 𝐴 = 𝐵

Proof of Theorem nfeq

Step	Hyp	Ref	Expression
1		nfnfc.1	. . . 4 ⊢ Ⅎ𝑥𝐴
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
3		nfeq.2	. . . 4 ⊢ Ⅎ𝑥𝐵
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐵)
5	2, 4	nfeqd 2976	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
6	5	mptru 1666	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1658  ⊤wtru 1659  Ⅎwnf 1884  Ⅎwnfc 2955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-cleq 2817  df-nfc 2957

This theorem is referenced by:  nfeq1  2982  nfeq2  2984  nfne  3098  raleqf  3345  rexeqf  3346  reueq1f  3347  rmoeq1f  3348  rabeqf  3402  csbhypf  3775  sbceqg  4207  nffn  6219  nffo  6351  fvmptd3f  6541  mpteqb  6545  fvmptf  6547  eqfnfv2f  6563  dff13f  6767  ovmpt2s  7043  ov2gf  7044  ovmpt2dxf  7045  ovmpt2df  7051  eqerlem  8042  seqof2  13152  sumeq2ii  14799  sumss  14831  fsumadd  14846  fsummulc2  14889  fsumrelem  14912  prodeq1f  15010  prodeq2ii  15015  fprodmul  15062  fproddiv  15063  fprodle  15098  txcnp  21793  ptcnplem  21794  cnmpt11  21836  cnmpt21  21844  cnmptcom  21851  mbfeqalem1  23806  mbflim  23833  itgeq1f  23936  itgeqa  23978  dvmptfsum  24136  ulmss  24549  leibpi  25081  o1cxp  25113  lgseisenlem2  25513  fmptcof2  30005  aciunf1lem  30010  sigapildsys  30769  bnj1316  31436  bnj1446  31658  bnj1447  31659  bnj1448  31660  bnj1519  31678  bnj1520  31679  bnj1529  31683  nosupbnd1  32398  subtr  32846  subtr2  32847  bj-sbeqALT  33415  poimirlem25  33977  iuneq2f  34502  mpt2bi123f  34510  mptbi12f  34514  dvdsrabdioph  38217  fphpd  38223  fvelrnbf  39994  refsum2cnlem1  40013  dffo3f  40171  elrnmptf  40174  disjrnmpt2  40182  disjinfi  40187  choicefi  40197  axccdom  40221  fvelimad  40258  uzublem  40451  fsumf1of  40600  fmuldfeq  40609  mccl  40624  climmulf  40630  climexp  40631  climsuse  40634  climrecf  40635  climaddf  40641  mullimc  40642  neglimc  40673  addlimc  40674  0ellimcdiv  40675  climeldmeqmpt  40694  climfveqmpt  40697  climfveqf  40706  climfveqmpt3  40708  climeldmeqf  40709  climeqf  40714  climeldmeqmpt3  40715  limsupubuzlem  40738  limsupequz  40749  dvnmptdivc  40947  dvmptfprod  40954  dvnprodlem1  40955  stoweidlem18  41028  stoweidlem31  41041  stoweidlem55  41065  stoweidlem59  41069  sge0f1o  41389  sge0iunmpt  41425  sge0reuz  41454  iundjiun  41467  hoicvrrex  41563  ovnhoilem1  41608  ovnlecvr2  41617  opnvonmbllem1  41639  vonioo  41689  vonicc  41692  sssmf  41740  smflim  41778  smfpimcclem  41806  smfpimcc  41807  ovmpt2rdxf  42963