Theorem nfeq 2922

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

Syntax hints:   = wceq 1537  ⊤wtru 1538  Ⅎwnf 1781  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-cleq 2732  df-nfc 2895

This theorem is referenced by:  nfeq1  2924  nfeq2  2926  nfne  3049  raleqf  3361  rexeqfOLD  3363  rmoeq1f  3431  rabeqf  3480  csbhypf  3950  sbceqg  4435  nffn  6678  nffo  6833  fvmptd3f  7044  mpteqb  7048  fvmptf  7050  eqfnfv2f  7068  dff13f  7293  ovmpos  7598  ov2gf  7599  ovmpodxf  7600  ovmpodf  7606  eqerlem  8798  seqof2  14111  sumeq2ii  15741  sumss  15772  fsumadd  15788  fsummulc2  15832  fsumrelem  15855  prodeq1f  15954  prodeq2ii  15959  fprodmul  16008  fproddiv  16009  txcnp  23649  ptcnplem  23650  cnmpt11  23692  cnmpt21  23700  cnmptcom  23707  mbfeqalem1  25695  mbflim  25722  itgeq1f  25826  itgeq1fOLD  25827  itgeqa  25869  dvmptfsum  26033  ulmss  26458  leibpi  27003  o1cxp  27036  lgseisenlem2  27438  nosupbnd1  27777  2ndresdju  32667  aciunf1lem  32680  sigapildsys  34126  bnj1316  34796  bnj1446  35021  bnj1447  35022  bnj1448  35023  bnj1519  35041  bnj1520  35042  bnj1529  35046  subtr  36280  subtr2  36281  bj-sbeqALT  36866  poimirlem25  37605  iuneq2f  38116  mpobi123f  38122  mptbi12f  38126  dvdsrabdioph  42766  fphpd  42772  mnringmulrcld  44197  fvelrnbf  44918  refsum2cnlem1  44937  elrnmpt1sf  45096  choicefi  45107  axccdom  45129  uzublem  45345  fsumf1of  45495  fmuldfeq  45504  mccl  45519  climmulf  45525  climexp  45526  climsuse  45529  climrecf  45530  climaddf  45536  mullimc  45537  neglimc  45568  addlimc  45569  0ellimcdiv  45570  climeldmeqmpt  45589  climfveqmpt  45592  climfveqf  45601  climfveqmpt3  45603  climeldmeqf  45604  climeqf  45609  climeldmeqmpt3  45610  limsupubuzlem  45633  limsupequz  45644  dvnmptdivc  45859  dvmptfprod  45866  dvnprodlem1  45867  stoweidlem18  45939  stoweidlem31  45952  stoweidlem55  45976  stoweidlem59  45980  sge0f1o  46303  sge0iunmpt  46339  sge0reuz  46368  iundjiun  46381  hoicvrrex  46477  ovnhoilem1  46522  ovnlecvr2  46531  opnvonmbllem1  46553  vonioo  46603  vonicc  46606  sssmf  46659  smflim  46698  smfpimcclem  46728  smfpimcc  46729  cfsetsnfsetf  46973  ovmpordxf  48063