Theorem nfeq 2913

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

Syntax hints:   = wceq 1542  ⊤wtru 1543  Ⅎwnf 1785  Ⅎwnfc 2884

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2729  df-nfc 2886

This theorem is referenced by:  nfeq1  2915  nfeq2  2917  nfne  3034  raleqf  3327  rexeqfOLD  3329  rmoeq1f  3391  rabeqf  3435  csbhypf  3879  sbceqg  4366  nffn  6599  nffo  6753  fvmptd3f  6965  mpteqb  6969  fvmptf  6971  eqfnfv2f  6989  dff13f  7211  ovmpos  7516  ov2gf  7517  ovmpodxf  7518  ovmpodf  7524  eqerlem  8681  seqof2  13995  sumeq2ii  15628  sumss  15659  fsumadd  15675  fsummulc2  15719  fsumrelem  15742  prodeq1f  15841  prodeq2ii  15846  fprodmul  15895  fproddiv  15896  txcnp  23576  ptcnplem  23577  cnmpt11  23619  cnmpt21  23627  cnmptcom  23634  mbfeqalem1  25610  mbflim  25637  itgeq1f  25740  itgeq1fOLD  25741  itgeqa  25783  dvmptfsum  25947  ulmss  26374  leibpi  26920  o1cxp  26953  lgseisenlem2  27355  nosupbnd1  27694  2ndresdju  32739  aciunf1lem  32752  deg1prod  33676  sigapildsys  34340  bnj1316  34996  bnj1446  35221  bnj1447  35222  bnj1448  35223  bnj1519  35241  bnj1520  35242  bnj1529  35246  subtr  36530  subtr2  36531  bj-sbeqALT  37148  poimirlem25  37896  iuneq2f  38407  mpobi123f  38413  mptbi12f  38417  dvdsrabdioph  43167  fphpd  43173  mnringmulrcld  44584  fvelrnbf  45378  refsum2cnlem1  45397  elrnmpt1sf  45548  choicefi  45558  axccdom  45580  uzublem  45788  fsumf1of  45934  fmuldfeq  45943  mccl  45958  climmulf  45964  climexp  45965  climsuse  45968  climrecf  45969  climaddf  45975  mullimc  45976  neglimc  46005  addlimc  46006  0ellimcdiv  46007  climeldmeqmpt  46026  climfveqmpt  46029  climfveqf  46038  climfveqmpt3  46040  climeldmeqf  46041  climeqf  46046  climeldmeqmpt3  46047  limsupubuzlem  46070  limsupequz  46081  dvnmptdivc  46296  dvmptfprod  46303  stoweidlem18  46376  stoweidlem31  46389  stoweidlem55  46413  stoweidlem59  46417  sge0iunmpt  46776  sge0reuz  46805  iundjiun  46818  hoicvrrex  46914  ovnhoilem1  46959  ovnlecvr2  46968  opnvonmbllem1  46990  vonioo  47040  vonicc  47043  sssmf  47096  smflim  47135  smfpimcclem  47165  smfpimcc  47166  cfsetsnfsetf  47418  ovmpordxf  48699