Theorem nfeq 2993

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

Syntax hints:   = wceq 1537  ⊤wtru 1538  Ⅎwnf 1784  Ⅎwnfc 2963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-cleq 2816  df-nfc 2965

This theorem is referenced by:  nfeq1  2995  nfeq2  2997  nfne  3121  raleqf  3399  rexeqf  3400  reueq1f  3401  rmoeq1f  3402  rabeqf  3483  csbhypf  3913  sbceqg  4363  nffn  6454  nffo  6591  fvmptd3f  6785  mpteqb  6789  fvmptf  6791  eqfnfv2f  6808  dff13f  7016  ovmpos  7300  ov2gf  7301  ovmpodxf  7302  ovmpodf  7308  eqerlem  8325  seqof2  13431  sumeq2ii  15052  sumss  15083  fsumadd  15098  fsummulc2  15141  fsumrelem  15164  prodeq1f  15264  prodeq2ii  15269  fprodmul  15316  fproddiv  15317  txcnp  22230  ptcnplem  22231  cnmpt11  22273  cnmpt21  22281  cnmptcom  22288  mbfeqalem1  24244  mbflim  24271  itgeq1f  24374  itgeqa  24416  dvmptfsum  24574  ulmss  24987  leibpi  25522  o1cxp  25554  lgseisenlem2  25954  aciunf1lem  30409  sigapildsys  31423  bnj1316  32094  bnj1446  32319  bnj1447  32320  bnj1448  32321  bnj1519  32339  bnj1520  32340  bnj1529  32344  nosupbnd1  33216  subtr  33664  subtr2  33665  bj-sbeqALT  34219  poimirlem25  34919  iuneq2f  35436  mpobi123f  35442  mptbi12f  35446  dvdsrabdioph  39414  fphpd  39420  fvelrnbf  41282  refsum2cnlem1  41301  elrnmpt1sf  41457  disjinfi  41461  choicefi  41470  axccdom  41494  uzublem  41711  fsumf1of  41862  fmuldfeq  41871  mccl  41886  climmulf  41892  climexp  41893  climsuse  41896  climrecf  41897  climaddf  41903  mullimc  41904  neglimc  41935  addlimc  41936  0ellimcdiv  41937  climeldmeqmpt  41956  climfveqmpt  41959  climfveqf  41968  climfveqmpt3  41970  climeldmeqf  41971  climeqf  41976  climeldmeqmpt3  41977  limsupubuzlem  42000  limsupequz  42011  dvnmptdivc  42230  dvmptfprod  42237  dvnprodlem1  42238  stoweidlem18  42310  stoweidlem31  42323  stoweidlem55  42347  stoweidlem59  42351  sge0f1o  42671  sge0iunmpt  42707  sge0reuz  42736  iundjiun  42749  hoicvrrex  42845  ovnhoilem1  42890  ovnlecvr2  42899  opnvonmbllem1  42921  vonioo  42971  vonicc  42974  sssmf  43022  smflim  43060  smfpimcclem  43088  smfpimcc  43089  ovmpordxf  44394