Theorem nfeq 2917

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-cleq 2725  df-nfc 2886

This theorem is referenced by:  nfeq1  2919  nfeq2  2921  nfne  3044  raleqf  3350  rexeqfOLD  3352  rmoeq1f  3421  rabeqf  3467  csbhypf  3923  sbceqg  4410  nffn  6649  nffo  6805  fvmptd3f  7014  mpteqb  7018  fvmptf  7020  eqfnfv2f  7037  dff13f  7255  ovmpos  7556  ov2gf  7557  ovmpodxf  7558  ovmpodf  7564  eqerlem  8737  seqof2  14026  sumeq2ii  15639  sumss  15670  fsumadd  15686  fsummulc2  15730  fsumrelem  15753  prodeq1f  15852  prodeq2ii  15857  fprodmul  15904  fproddiv  15905  txcnp  23124  ptcnplem  23125  cnmpt11  23167  cnmpt21  23175  cnmptcom  23182  mbfeqalem1  25158  mbflim  25185  itgeq1f  25289  itgeqa  25331  dvmptfsum  25492  ulmss  25909  leibpi  26447  o1cxp  26479  lgseisenlem2  26879  nosupbnd1  27217  2ndresdju  31874  aciunf1lem  31887  sigapildsys  33160  bnj1316  33831  bnj1446  34056  bnj1447  34057  bnj1448  34058  bnj1519  34076  bnj1520  34077  bnj1529  34081  subtr  35199  subtr2  35200  bj-sbeqALT  35780  poimirlem25  36513  iuneq2f  37024  mpobi123f  37030  mptbi12f  37034  dvdsrabdioph  41548  fphpd  41554  mnringmulrcld  42987  fvelrnbf  43702  refsum2cnlem1  43721  elrnmpt1sf  43887  choicefi  43899  axccdom  43921  uzublem  44140  fsumf1of  44290  fmuldfeq  44299  mccl  44314  climmulf  44320  climexp  44321  climsuse  44324  climrecf  44325  climaddf  44331  mullimc  44332  neglimc  44363  addlimc  44364  0ellimcdiv  44365  climeldmeqmpt  44384  climfveqmpt  44387  climfveqf  44396  climfveqmpt3  44398  climeldmeqf  44399  climeqf  44404  climeldmeqmpt3  44405  limsupubuzlem  44428  limsupequz  44439  dvnmptdivc  44654  dvmptfprod  44661  dvnprodlem1  44662  stoweidlem18  44734  stoweidlem31  44747  stoweidlem55  44771  stoweidlem59  44775  sge0f1o  45098  sge0iunmpt  45134  sge0reuz  45163  iundjiun  45176  hoicvrrex  45272  ovnhoilem1  45317  ovnlecvr2  45326  opnvonmbllem1  45348  vonioo  45398  vonicc  45401  sssmf  45454  smflim  45493  smfpimcclem  45523  smfpimcc  45524  cfsetsnfsetf  45768  ovmpordxf  47014