Theorem nfeq 2919

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

Syntax hints:   = wceq 1539  ⊤wtru 1540  Ⅎwnf 1787  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-nf 1788  df-cleq 2730  df-nfc 2888

This theorem is referenced by:  nfeq1  2921  nfeq2  2923  nfne  3044  raleqf  3323  rexeqf  3324  reueq1f  3325  rmoeq1f  3326  rabeqf  3405  csbhypf  3857  sbceqg  4340  nffn  6516  nffo  6671  fvmptd3f  6872  mpteqb  6876  fvmptf  6878  eqfnfv2f  6895  dff13f  7110  ovmpos  7399  ov2gf  7400  ovmpodxf  7401  ovmpodf  7407  eqerlem  8490  seqof2  13709  sumeq2ii  15333  sumss  15364  fsumadd  15380  fsummulc2  15424  fsumrelem  15447  prodeq1f  15546  prodeq2ii  15551  fprodmul  15598  fproddiv  15599  txcnp  22679  ptcnplem  22680  cnmpt11  22722  cnmpt21  22730  cnmptcom  22737  mbfeqalem1  24710  mbflim  24737  itgeq1f  24841  itgeqa  24883  dvmptfsum  25044  ulmss  25461  leibpi  25997  o1cxp  26029  lgseisenlem2  26429  2ndresdju  30887  aciunf1lem  30901  sigapildsys  32030  bnj1316  32700  bnj1446  32925  bnj1447  32926  bnj1448  32927  bnj1519  32945  bnj1520  32946  bnj1529  32950  nosupbnd1  33844  subtr  34430  subtr2  34431  bj-sbeqALT  35012  poimirlem25  35729  iuneq2f  36241  mpobi123f  36247  mptbi12f  36251  dvdsrabdioph  40548  fphpd  40554  mnringmulrcld  41735  fvelrnbf  42450  refsum2cnlem1  42469  elrnmpt1sf  42616  choicefi  42629  axccdom  42651  uzublem  42860  fsumf1of  43005  fmuldfeq  43014  mccl  43029  climmulf  43035  climexp  43036  climsuse  43039  climrecf  43040  climaddf  43046  mullimc  43047  neglimc  43078  addlimc  43079  0ellimcdiv  43080  climeldmeqmpt  43099  climfveqmpt  43102  climfveqf  43111  climfveqmpt3  43113  climeldmeqf  43114  climeqf  43119  climeldmeqmpt3  43120  limsupubuzlem  43143  limsupequz  43154  dvnmptdivc  43369  dvmptfprod  43376  dvnprodlem1  43377  stoweidlem18  43449  stoweidlem31  43462  stoweidlem55  43486  stoweidlem59  43490  sge0f1o  43810  sge0iunmpt  43846  sge0reuz  43875  iundjiun  43888  hoicvrrex  43984  ovnhoilem1  44029  ovnlecvr2  44038  opnvonmbllem1  44060  vonioo  44110  vonicc  44113  sssmf  44161  smflim  44199  smfpimcclem  44227  smfpimcc  44228  cfsetsnfsetf  44439  ovmpordxf  45562