Theorem nfeq 2968

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

Syntax hints:   = wceq 1538  ⊤wtru 1539  Ⅎwnf 1785  Ⅎwnfc 2936

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-cleq 2791  df-nfc 2938

This theorem is referenced by:  nfeq1  2970  nfeq2  2972  nfne  3087  raleqf  3350  rexeqf  3351  reueq1f  3352  rmoeq1f  3353  rabeqf  3428  csbhypf  3856  sbceqg  4317  nffn  6422  nffo  6564  fvmptd3f  6760  mpteqb  6764  fvmptf  6766  eqfnfv2f  6783  dff13f  6992  ovmpos  7277  ov2gf  7278  ovmpodxf  7279  ovmpodf  7285  eqerlem  8306  seqof2  13424  sumeq2ii  15042  sumss  15073  fsumadd  15088  fsummulc2  15131  fsumrelem  15154  prodeq1f  15254  prodeq2ii  15259  fprodmul  15306  fproddiv  15307  txcnp  22225  ptcnplem  22226  cnmpt11  22268  cnmpt21  22276  cnmptcom  22283  mbfeqalem1  24245  mbflim  24272  itgeq1f  24375  itgeqa  24417  dvmptfsum  24578  ulmss  24992  leibpi  25528  o1cxp  25560  lgseisenlem2  25960  2ndresdju  30411  aciunf1lem  30425  sigapildsys  31531  bnj1316  32202  bnj1446  32427  bnj1447  32428  bnj1448  32429  bnj1519  32447  bnj1520  32448  bnj1529  32452  nosupbnd1  33327  subtr  33775  subtr2  33776  bj-sbeqALT  34341  poimirlem25  35082  iuneq2f  35594  mpobi123f  35600  mptbi12f  35604  dvdsrabdioph  39751  fphpd  39757  mnringmulrcld  40936  fvelrnbf  41647  refsum2cnlem1  41666  elrnmpt1sf  41816  choicefi  41829  axccdom  41853  uzublem  42067  fsumf1of  42216  fmuldfeq  42225  mccl  42240  climmulf  42246  climexp  42247  climsuse  42250  climrecf  42251  climaddf  42257  mullimc  42258  neglimc  42289  addlimc  42290  0ellimcdiv  42291  climeldmeqmpt  42310  climfveqmpt  42313  climfveqf  42322  climfveqmpt3  42324  climeldmeqf  42325  climeqf  42330  climeldmeqmpt3  42331  limsupubuzlem  42354  limsupequz  42365  dvnmptdivc  42580  dvmptfprod  42587  dvnprodlem1  42588  stoweidlem18  42660  stoweidlem31  42673  stoweidlem55  42697  stoweidlem59  42701  sge0f1o  43021  sge0iunmpt  43057  sge0reuz  43086  iundjiun  43099  hoicvrrex  43195  ovnhoilem1  43240  ovnlecvr2  43249  opnvonmbllem1  43271  vonioo  43321  vonicc  43324  sssmf  43372  smflim  43410  smfpimcclem  43438  smfpimcc  43439  ovmpordxf  44740