Theorem nfeq 2944

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

Syntax hints:   = wceq 1567  ⊤wtru 1568  Ⅎwnf 1810  Ⅎwnfc 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-cleq 2761  df-nfc 2918

This theorem is referenced by:  nfeq1  2946  nfeq2  2948  nfne  3067  raleqf  3352  rmoeq1f  3413  rabeqf  3457  csbhypf  3889  sbceqg  4383  nffn  6635  nffo  6792  fvmptd3f  7006  mpteqb  7010  fvmptf  7012  eqfnfv2f  7030  dff13f  7254  ovmpos  7559  ov2gf  7560  ovmpodxf  7561  ovmpodf  7567  eqerlem  8729  seqof2  14095  sumeq2ii  15743  sumss  15774  fsumadd  15790  fsummulc2  15834  fsumrelem  15858  prodeq1f  15959  prodeq2ii  15964  fprodmul  16013  fproddiv  16014  txcnp  23745  ptcnplem  23746  cnmpt11  23788  cnmpt21  23796  cnmptcom  23803  mbfeqalem1  25768  mbflim  25795  itgeq1f  25898  itgeq1fOLD  25899  itgeqa  25941  dvmptfsum  26102  ulmss  26525  leibpi  27072  o1cxp  27104  lgseisenlem2  27505  nosupbnd1  27843  2ndresdju  32934  aciunf1lem  32947  deg1prod  33817  sigapildsys  34496  bnj1316  35152  bnj1446  35377  bnj1447  35378  bnj1448  35379  bnj1519  35397  bnj1520  35398  bnj1529  35402  subtr  36713  subtr2  36714  bj-sbeqALT  37423  poimirlem25  38183  iuneq2f  38694  mpobi123f  38700  mptbi12f  38704  dvdsrabdioph  43428  fphpd  43434  mnringmulrcld  44843  fvelrnbf  45629  refsum2cnlem1  45648  elrnmpt1sf  45798  choicefi  45808  axccdom  45829  uzublem  46035  fsumf1of  46181  fmuldfeq  46190  mccl  46205  climmulf  46211  climexp  46212  climsuse  46215  climrecf  46216  climaddf  46222  mullimc  46223  neglimc  46252  addlimc  46253  0ellimcdiv  46254  climeldmeqmpt  46273  climfveqmpt  46276  climfveqf  46285  climfveqmpt3  46287  climeldmeqf  46288  climeqf  46293  climeldmeqmpt3  46294  limsupubuzlem  46317  limsupequz  46328  dvnmptdivc  46543  dvmptfprod  46550  stoweidlem18  46623  stoweidlem31  46636  stoweidlem55  46660  stoweidlem59  46664  sge0iunmpt  47023  sge0reuz  47052  iundjiun  47065  hoicvrrex  47161  ovnhoilem1  47206  ovnlecvr2  47215  opnvonmbllem1  47237  vonioo  47287  vonicc  47290  smflim  47382  smfpimcclem  47412  smfpimcc  47413  cfsetsnfsetf  47683  ovmpordxf  49003