Theorem nfeq 2906

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	trud 1634	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1624  ⊤wtru 1625  Ⅎwnf 1849  Ⅎwnfc 2881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-cleq 2745  df-nfc 2883

This theorem is referenced by:  nfeq1  2908  nfeq2  2910  nfne  3024  raleqf  3265  rexeqf  3266  reueq1f  3267  rmoeq1f  3268  rabeqf  3322  csbhypf  3685  sbceqg  4119  nffn  6140  nffo  6267  fvmptd3f  6449  mpteqb  6453  fvmptf  6455  eqfnfv2f  6470  dff13f  6668  ovmpt2s  6941  ov2gf  6942  ovmpt2dxf  6943  ovmpt2df  6949  eqerlem  7937  seqof2  13045  sumeq2ii  14614  sumss  14646  fsumadd  14661  fsummulc2  14707  fsumrelem  14730  prodeq1f  14829  prodeq2ii  14834  fprodmul  14881  fproddiv  14882  fprodle  14918  txcnp  21617  ptcnplem  21618  cnmpt11  21660  cnmpt21  21668  cnmptcom  21675  mbfeqalem  23600  mbflim  23626  itgeq1f  23729  itgeqa  23771  dvmptfsum  23929  ulmss  24342  leibpi  24860  o1cxp  24892  lgseisenlem2  25292  fmptcof2  29758  aciunf1lem  29763  sigapildsys  30526  bnj1316  31190  bnj1446  31412  bnj1447  31413  bnj1448  31414  bnj1519  31432  bnj1520  31433  bnj1529  31437  nosupbnd1  32158  subtr  32606  subtr2  32607  bj-sbeqALT  33193  poimirlem25  33739  iuneq2f  34268  mpt2bi123f  34276  mptbi12f  34280  dvdsrabdioph  37868  fphpd  37874  fvelrnbf  39668  refsum2cnlem1  39687  dffo3f  39855  elrnmptf  39858  disjrnmpt2  39866  disjinfi  39871  choicefi  39883  axccdom  39907  fvelimad  39949  uzublem  40147  fsumf1of  40301  fmuldfeq  40310  mccl  40325  climmulf  40331  climexp  40332  climsuse  40335  climrecf  40336  climaddf  40342  mullimc  40343  neglimc  40374  addlimc  40375  0ellimcdiv  40376  climeldmeqmpt  40395  climfveqmpt  40398  climfveqf  40407  climfveqmpt3  40409  climeldmeqf  40410  climeqf  40415  climeldmeqmpt3  40416  limsupubuzlem  40439  limsupequz  40450  dvnmptdivc  40648  dvmptfprod  40655  dvnprodlem1  40656  stoweidlem18  40730  stoweidlem31  40743  stoweidlem55  40767  stoweidlem59  40771  sge0f1o  41094  sge0iunmpt  41130  sge0reuz  41159  iundjiun  41172  hoicvrrex  41268  ovnhoilem1  41313  ovnlecvr2  41322  opnvonmbllem1  41344  vonioo  41394  vonicc  41397  sssmf  41445  smflim  41483  smfpimcclem  41511  smfpimcc  41512  ovmpt2rdxf  42619