Theorem nfeq 2915

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 2912	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
6	5	mptru 1548	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1541  ⊤wtru 1542  Ⅎwnf 1785  Ⅎwnfc 2882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-cleq 2723  df-nfc 2884

This theorem is referenced by:  nfeq1  2917  nfeq2  2919  nfne  3042  raleqf  3326  rexeqf  3327  rmoeq1f  3393  reueq1f  3394  rabeqf  3439  csbhypf  3887  sbceqg  4374  nffn  6606  nffo  6760  fvmptd3f  6968  mpteqb  6972  fvmptf  6974  eqfnfv2f  6991  dff13f  7208  ovmpos  7508  ov2gf  7509  ovmpodxf  7510  ovmpodf  7516  eqerlem  8689  seqof2  13976  sumeq2ii  15589  sumss  15620  fsumadd  15636  fsummulc2  15680  fsumrelem  15703  prodeq1f  15802  prodeq2ii  15807  fprodmul  15854  fproddiv  15855  txcnp  23008  ptcnplem  23009  cnmpt11  23051  cnmpt21  23059  cnmptcom  23066  mbfeqalem1  25042  mbflim  25069  itgeq1f  25173  itgeqa  25215  dvmptfsum  25376  ulmss  25793  leibpi  26329  o1cxp  26361  lgseisenlem2  26761  nosupbnd1  27099  2ndresdju  31632  aciunf1lem  31645  sigapildsys  32850  bnj1316  33521  bnj1446  33746  bnj1447  33747  bnj1448  33748  bnj1519  33766  bnj1520  33767  bnj1529  33771  subtr  34862  subtr2  34863  bj-sbeqALT  35443  poimirlem25  36176  iuneq2f  36688  mpobi123f  36694  mptbi12f  36698  dvdsrabdioph  41191  fphpd  41197  mnringmulrcld  42630  fvelrnbf  43345  refsum2cnlem1  43364  elrnmpt1sf  43530  choicefi  43542  axccdom  43564  uzublem  43785  fsumf1of  43935  fmuldfeq  43944  mccl  43959  climmulf  43965  climexp  43966  climsuse  43969  climrecf  43970  climaddf  43976  mullimc  43977  neglimc  44008  addlimc  44009  0ellimcdiv  44010  climeldmeqmpt  44029  climfveqmpt  44032  climfveqf  44041  climfveqmpt3  44043  climeldmeqf  44044  climeqf  44049  climeldmeqmpt3  44050  limsupubuzlem  44073  limsupequz  44084  dvnmptdivc  44299  dvmptfprod  44306  dvnprodlem1  44307  stoweidlem18  44379  stoweidlem31  44392  stoweidlem55  44416  stoweidlem59  44420  sge0f1o  44743  sge0iunmpt  44779  sge0reuz  44808  iundjiun  44821  hoicvrrex  44917  ovnhoilem1  44962  ovnlecvr2  44971  opnvonmbllem1  44993  vonioo  45043  vonicc  45046  sssmf  45099  smflim  45138  smfpimcclem  45168  smfpimcc  45169  cfsetsnfsetf  45412  ovmpordxf  46534