Theorem nfeq 2905

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

Syntax hints:   = wceq 1540  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2721  df-nfc 2878

This theorem is referenced by:  nfeq1  2907  nfeq2  2909  nfne  3026  raleqf  3329  rexeqfOLD  3331  rmoeq1f  3395  rabeqf  3440  csbhypf  3890  sbceqg  4375  nffn  6617  nffo  6771  fvmptd3f  6983  mpteqb  6987  fvmptf  6989  eqfnfv2f  7007  dff13f  7230  ovmpos  7537  ov2gf  7538  ovmpodxf  7539  ovmpodf  7545  eqerlem  8706  seqof2  14025  sumeq2ii  15659  sumss  15690  fsumadd  15706  fsummulc2  15750  fsumrelem  15773  prodeq1f  15872  prodeq2ii  15877  fprodmul  15926  fproddiv  15927  txcnp  23507  ptcnplem  23508  cnmpt11  23550  cnmpt21  23558  cnmptcom  23565  mbfeqalem1  25542  mbflim  25569  itgeq1f  25672  itgeq1fOLD  25673  itgeqa  25715  dvmptfsum  25879  ulmss  26306  leibpi  26852  o1cxp  26885  lgseisenlem2  27287  nosupbnd1  27626  2ndresdju  32573  aciunf1lem  32586  sigapildsys  34152  bnj1316  34810  bnj1446  35035  bnj1447  35036  bnj1448  35037  bnj1519  35055  bnj1520  35056  bnj1529  35060  subtr  36302  subtr2  36303  bj-sbeqALT  36888  poimirlem25  37639  iuneq2f  38150  mpobi123f  38156  mptbi12f  38160  dvdsrabdioph  42798  fphpd  42804  mnringmulrcld  44217  fvelrnbf  45012  refsum2cnlem1  45031  elrnmpt1sf  45183  choicefi  45194  axccdom  45216  uzublem  45426  fsumf1of  45572  fmuldfeq  45581  mccl  45596  climmulf  45602  climexp  45603  climsuse  45606  climrecf  45607  climaddf  45613  mullimc  45614  neglimc  45645  addlimc  45646  0ellimcdiv  45647  climeldmeqmpt  45666  climfveqmpt  45669  climfveqf  45678  climfveqmpt3  45680  climeldmeqf  45681  climeqf  45686  climeldmeqmpt3  45687  limsupubuzlem  45710  limsupequz  45721  dvnmptdivc  45936  dvmptfprod  45943  stoweidlem18  46016  stoweidlem31  46029  stoweidlem55  46053  stoweidlem59  46057  sge0iunmpt  46416  sge0reuz  46445  iundjiun  46458  hoicvrrex  46554  ovnhoilem1  46599  ovnlecvr2  46608  opnvonmbllem1  46630  vonioo  46680  vonicc  46683  sssmf  46736  smflim  46775  smfpimcclem  46805  smfpimcc  46806  cfsetsnfsetf  47056  ovmpordxf  48324