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  3326  rexeqfOLD  3328  rmoeq1f  3392  rabeqf  3437  csbhypf  3887  sbceqg  4371  nffn  6599  nffo  6753  fvmptd3f  6965  mpteqb  6969  fvmptf  6971  eqfnfv2f  6989  dff13f  7212  ovmpos  7517  ov2gf  7518  ovmpodxf  7519  ovmpodf  7525  eqerlem  8683  seqof2  14001  sumeq2ii  15635  sumss  15666  fsumadd  15682  fsummulc2  15726  fsumrelem  15749  prodeq1f  15848  prodeq2ii  15853  fprodmul  15902  fproddiv  15903  txcnp  23540  ptcnplem  23541  cnmpt11  23583  cnmpt21  23591  cnmptcom  23598  mbfeqalem1  25575  mbflim  25602  itgeq1f  25705  itgeq1fOLD  25706  itgeqa  25748  dvmptfsum  25912  ulmss  26339  leibpi  26885  o1cxp  26918  lgseisenlem2  27320  nosupbnd1  27659  2ndresdju  32623  aciunf1lem  32636  sigapildsys  34145  bnj1316  34803  bnj1446  35028  bnj1447  35029  bnj1448  35030  bnj1519  35048  bnj1520  35049  bnj1529  35053  subtr  36295  subtr2  36296  bj-sbeqALT  36881  poimirlem25  37632  iuneq2f  38143  mpobi123f  38149  mptbi12f  38153  dvdsrabdioph  42791  fphpd  42797  mnringmulrcld  44210  fvelrnbf  45005  refsum2cnlem1  45024  elrnmpt1sf  45176  choicefi  45187  axccdom  45209  uzublem  45419  fsumf1of  45565  fmuldfeq  45574  mccl  45589  climmulf  45595  climexp  45596  climsuse  45599  climrecf  45600  climaddf  45606  mullimc  45607  neglimc  45638  addlimc  45639  0ellimcdiv  45640  climeldmeqmpt  45659  climfveqmpt  45662  climfveqf  45671  climfveqmpt3  45673  climeldmeqf  45674  climeqf  45679  climeldmeqmpt3  45680  limsupubuzlem  45703  limsupequz  45714  dvnmptdivc  45929  dvmptfprod  45936  stoweidlem18  46009  stoweidlem31  46022  stoweidlem55  46046  stoweidlem59  46050  sge0iunmpt  46409  sge0reuz  46438  iundjiun  46451  hoicvrrex  46547  ovnhoilem1  46592  ovnlecvr2  46601  opnvonmbllem1  46623  vonioo  46673  vonicc  46676  sssmf  46729  smflim  46768  smfpimcclem  46798  smfpimcc  46799  cfsetsnfsetf  47052  ovmpordxf  48320