Theorem nfeq 2908

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

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

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 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

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 2723  df-nfc 2881

This theorem is referenced by:  nfeq1  2910  nfeq2  2912  nfne  3029  raleqf  3321  rexeqfOLD  3323  rmoeq1f  3385  rabeqf  3429  csbhypf  3873  sbceqg  4359  nffn  6580  nffo  6734  fvmptd3f  6944  mpteqb  6948  fvmptf  6950  eqfnfv2f  6968  dff13f  7189  ovmpos  7494  ov2gf  7495  ovmpodxf  7496  ovmpodf  7502  eqerlem  8657  seqof2  13967  sumeq2ii  15600  sumss  15631  fsumadd  15647  fsummulc2  15691  fsumrelem  15714  prodeq1f  15813  prodeq2ii  15818  fprodmul  15867  fproddiv  15868  txcnp  23535  ptcnplem  23536  cnmpt11  23578  cnmpt21  23586  cnmptcom  23593  mbfeqalem1  25569  mbflim  25596  itgeq1f  25699  itgeq1fOLD  25700  itgeqa  25742  dvmptfsum  25906  ulmss  26333  leibpi  26879  o1cxp  26912  lgseisenlem2  27314  nosupbnd1  27653  2ndresdju  32631  aciunf1lem  32644  sigapildsys  34175  bnj1316  34832  bnj1446  35057  bnj1447  35058  bnj1448  35059  bnj1519  35077  bnj1520  35078  bnj1529  35082  subtr  36356  subtr2  36357  bj-sbeqALT  36942  poimirlem25  37693  iuneq2f  38204  mpobi123f  38210  mptbi12f  38214  dvdsrabdioph  42851  fphpd  42857  mnringmulrcld  44269  fvelrnbf  45063  refsum2cnlem1  45082  elrnmpt1sf  45234  choicefi  45245  axccdom  45267  uzublem  45476  fsumf1of  45622  fmuldfeq  45631  mccl  45646  climmulf  45652  climexp  45653  climsuse  45656  climrecf  45657  climaddf  45663  mullimc  45664  neglimc  45693  addlimc  45694  0ellimcdiv  45695  climeldmeqmpt  45714  climfveqmpt  45717  climfveqf  45726  climfveqmpt3  45728  climeldmeqf  45729  climeqf  45734  climeldmeqmpt3  45735  limsupubuzlem  45758  limsupequz  45769  dvnmptdivc  45984  dvmptfprod  45991  stoweidlem18  46064  stoweidlem31  46077  stoweidlem55  46101  stoweidlem59  46105  sge0iunmpt  46464  sge0reuz  46493  iundjiun  46506  hoicvrrex  46602  ovnhoilem1  46647  ovnlecvr2  46656  opnvonmbllem1  46678  vonioo  46728  vonicc  46731  sssmf  46784  smflim  46823  smfpimcclem  46853  smfpimcc  46854  cfsetsnfsetf  47097  ovmpordxf  48378