Theorem nfeq 2910

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

Syntax hints:   = wceq 1541  ⊤wtru 1542  Ⅎwnf 1784  Ⅎwnfc 2881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2726  df-nfc 2883

This theorem is referenced by:  nfeq1  2912  nfeq2  2914  nfne  3031  raleqf  3323  rexeqfOLD  3325  rmoeq1f  3387  rabeqf  3431  csbhypf  3875  sbceqg  4362  nffn  6589  nffo  6743  fvmptd3f  6954  mpteqb  6958  fvmptf  6960  eqfnfv2f  6978  dff13f  7199  ovmpos  7504  ov2gf  7505  ovmpodxf  7506  ovmpodf  7512  eqerlem  8668  seqof2  13981  sumeq2ii  15614  sumss  15645  fsumadd  15661  fsummulc2  15705  fsumrelem  15728  prodeq1f  15827  prodeq2ii  15832  fprodmul  15881  fproddiv  15882  txcnp  23562  ptcnplem  23563  cnmpt11  23605  cnmpt21  23613  cnmptcom  23620  mbfeqalem1  25596  mbflim  25623  itgeq1f  25726  itgeq1fOLD  25727  itgeqa  25769  dvmptfsum  25933  ulmss  26360  leibpi  26906  o1cxp  26939  lgseisenlem2  27341  nosupbnd1  27680  2ndresdju  32676  aciunf1lem  32689  deg1prod  33613  sigapildsys  34268  bnj1316  34925  bnj1446  35150  bnj1447  35151  bnj1448  35152  bnj1519  35170  bnj1520  35171  bnj1529  35175  subtr  36457  subtr2  36458  bj-sbeqALT  37044  poimirlem25  37785  iuneq2f  38296  mpobi123f  38302  mptbi12f  38306  dvdsrabdioph  42994  fphpd  43000  mnringmulrcld  44411  fvelrnbf  45205  refsum2cnlem1  45224  elrnmpt1sf  45375  choicefi  45386  axccdom  45408  uzublem  45616  fsumf1of  45762  fmuldfeq  45771  mccl  45786  climmulf  45792  climexp  45793  climsuse  45796  climrecf  45797  climaddf  45803  mullimc  45804  neglimc  45833  addlimc  45834  0ellimcdiv  45835  climeldmeqmpt  45854  climfveqmpt  45857  climfveqf  45866  climfveqmpt3  45868  climeldmeqf  45869  climeqf  45874  climeldmeqmpt3  45875  limsupubuzlem  45898  limsupequz  45909  dvnmptdivc  46124  dvmptfprod  46131  stoweidlem18  46204  stoweidlem31  46217  stoweidlem55  46241  stoweidlem59  46245  sge0iunmpt  46604  sge0reuz  46633  iundjiun  46646  hoicvrrex  46742  ovnhoilem1  46787  ovnlecvr2  46796  opnvonmbllem1  46818  vonioo  46868  vonicc  46871  sssmf  46924  smflim  46963  smfpimcclem  46993  smfpimcc  46994  cfsetsnfsetf  47246  ovmpordxf  48527