Theorem nfeq 2916

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

Syntax hints:   = wceq 1536  ⊤wtru 1537  Ⅎwnf 1779  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-nf 1780  df-cleq 2726  df-nfc 2889

This theorem is referenced by:  nfeq1  2918  nfeq2  2920  nfne  3040  raleqf  3350  rexeqfOLD  3352  rmoeq1f  3420  rabeqf  3469  csbhypf  3936  sbceqg  4417  nffn  6667  nffo  6819  fvmptd3f  7030  mpteqb  7034  fvmptf  7036  eqfnfv2f  7054  dff13f  7275  ovmpos  7580  ov2gf  7581  ovmpodxf  7582  ovmpodf  7588  eqerlem  8778  seqof2  14097  sumeq2ii  15725  sumss  15756  fsumadd  15772  fsummulc2  15816  fsumrelem  15839  prodeq1f  15938  prodeq2ii  15943  fprodmul  15992  fproddiv  15993  txcnp  23643  ptcnplem  23644  cnmpt11  23686  cnmpt21  23694  cnmptcom  23701  mbfeqalem1  25689  mbflim  25716  itgeq1f  25820  itgeq1fOLD  25821  itgeqa  25863  dvmptfsum  26027  ulmss  26454  leibpi  26999  o1cxp  27032  lgseisenlem2  27434  nosupbnd1  27773  2ndresdju  32665  aciunf1lem  32678  sigapildsys  34142  bnj1316  34812  bnj1446  35037  bnj1447  35038  bnj1448  35039  bnj1519  35057  bnj1520  35058  bnj1529  35062  subtr  36296  subtr2  36297  bj-sbeqALT  36882  poimirlem25  37631  iuneq2f  38142  mpobi123f  38148  mptbi12f  38152  dvdsrabdioph  42797  fphpd  42803  mnringmulrcld  44223  fvelrnbf  44955  refsum2cnlem1  44974  elrnmpt1sf  45131  choicefi  45142  axccdom  45164  uzublem  45379  fsumf1of  45529  fmuldfeq  45538  mccl  45553  climmulf  45559  climexp  45560  climsuse  45563  climrecf  45564  climaddf  45570  mullimc  45571  neglimc  45602  addlimc  45603  0ellimcdiv  45604  climeldmeqmpt  45623  climfveqmpt  45626  climfveqf  45635  climfveqmpt3  45637  climeldmeqf  45638  climeqf  45643  climeldmeqmpt3  45644  limsupubuzlem  45667  limsupequz  45678  dvnmptdivc  45893  dvmptfprod  45900  stoweidlem18  45973  stoweidlem31  45986  stoweidlem55  46010  stoweidlem59  46014  sge0iunmpt  46373  sge0reuz  46402  iundjiun  46415  hoicvrrex  46511  ovnhoilem1  46556  ovnlecvr2  46565  opnvonmbllem1  46587  vonioo  46637  vonicc  46640  sssmf  46693  smflim  46732  smfpimcclem  46762  smfpimcc  46763  cfsetsnfsetf  47007  ovmpordxf  48183