Theorem nfeq 2914

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

Syntax hints:   = wceq 1547  ⊤wtru 1548  Ⅎwnf 1790  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-cleq 2731  df-nfc 2888

This theorem is referenced by:  nfeq1  2916  nfeq2  2918  nfne  3035  raleqf  3320  rmoeq1f  3381  rabeqf  3425  csbhypf  3859  sbceqg  4340  nffn  6584  nffo  6738  fvmptd3f  6951  mpteqb  6955  fvmptf  6957  eqfnfv2f  6975  dff13f  7199  ovmpos  7504  ov2gf  7505  ovmpodxf  7506  ovmpodf  7512  eqerlem  8669  seqof2  14013  sumeq2ii  15646  sumss  15677  fsumadd  15693  fsummulc2  15737  fsumrelem  15761  prodeq1f  15862  prodeq2ii  15867  fprodmul  15916  fproddiv  15917  txcnp  23603  ptcnplem  23604  cnmpt11  23646  cnmpt21  23654  cnmptcom  23661  mbfeqalem1  25626  mbflim  25653  itgeq1f  25756  itgeq1fOLD  25757  itgeqa  25799  dvmptfsum  25960  ulmss  26380  leibpi  26924  o1cxp  26956  lgseisenlem2  27357  nosupbnd1  27696  2ndresdju  32741  aciunf1lem  32754  deg1prod  33666  sigapildsys  34346  bnj1316  35002  bnj1446  35227  bnj1447  35228  bnj1448  35229  bnj1519  35247  bnj1520  35248  bnj1529  35252  subtr  36542  subtr2  36543  bj-sbeqALT  37253  poimirlem25  38012  iuneq2f  38523  mpobi123f  38529  mptbi12f  38533  dvdsrabdioph  43255  fphpd  43261  mnringmulrcld  44672  fvelrnbf  45466  refsum2cnlem1  45485  elrnmpt1sf  45636  choicefi  45646  axccdom  45667  uzublem  45873  fsumf1of  46019  fmuldfeq  46028  mccl  46043  climmulf  46049  climexp  46050  climsuse  46053  climrecf  46054  climaddf  46060  mullimc  46061  neglimc  46090  addlimc  46091  0ellimcdiv  46092  climeldmeqmpt  46111  climfveqmpt  46114  climfveqf  46123  climfveqmpt3  46125  climeldmeqf  46126  climeqf  46131  climeldmeqmpt3  46132  limsupubuzlem  46155  limsupequz  46166  dvnmptdivc  46381  dvmptfprod  46388  stoweidlem18  46461  stoweidlem31  46474  stoweidlem55  46498  stoweidlem59  46502  sge0iunmpt  46861  sge0reuz  46890  iundjiun  46903  hoicvrrex  46999  ovnhoilem1  47044  ovnlecvr2  47053  opnvonmbllem1  47075  vonioo  47125  vonicc  47128  sssmf  47181  smflim  47220  smfpimcclem  47250  smfpimcc  47251  cfsetsnfsetf  47521  ovmpordxf  48830