Theorem nfeq 2657

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 2653	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
6	5	trud 1477	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1468  ⊤wtru 1469  Ⅎwnf 1696  Ⅎwnfc 2633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-ext 2485

This theorem depends on definitions:  df-bi 192  df-an 380  df-tru 1471  df-ex 1693  df-nf 1697  df-cleq 2498  df-nfc 2635

This theorem is referenced by:  nfeq1  2659  nfeq2  2661  nfne  2777  raleqf  3004  rexeqf  3005  reueq1f  3006  rmoeq1f  3007  rabeqf  3058  csbhypf  3404  sbceqg  3813  nffn  5727  nffo  5851  fvmptdf  6028  mpteqb  6031  fvmptf  6033  eqfnfv2f  6047  dff13f  6231  ovmpt2s  6495  ov2gf  6496  ovmpt2dxf  6497  ovmpt2df  6503  eqerlem  7474  seqof2  12385  sumeq2ii  13919  sumss  13950  fsumadd  13965  fsummulc2  14005  fsumrelem  14027  prodeq1f  14122  prodeq2ii  14127  fprodmul  14174  fproddiv  14175  fprodle  14210  txcnp  20792  ptcnplem  20793  cnmpt11  20835  cnmpt21  20843  cnmptcom  20850  mbfeqalem  22759  mbflim  22787  itgeq1f  22890  itgeqa  22932  dvmptfsum  23088  ulmss  23513  leibpi  24029  o1cxp  24061  lgseisenlem2  24439  fmptcof2  28416  aciunf1lem  28421  sigapildsys  29139  oms0OLD  29283  bnj1316  29784  bnj1446  30006  bnj1447  30007  bnj1448  30008  bnj1519  30026  bnj1520  30027  bnj1529  30031  subtr  31119  subtr2  31120  bj-sbeqALT  31686  poimirlem25  32203  iuneq2f  32634  mpt2bi123f  32642  mptbi12f  32646  dvdsrabdioph  35893  fphpd  35899  fvelrnbf  37687  refsum2cnlem1  37706  dffo3f  37811  elrnmptf  37814  disjrnmpt2  37823  disjinfi  37828  choicefi  37840  fsumf1of  38054  fmuldfeq  38063  mccl  38080  climmulf  38086  climexp  38087  climsuse  38091  climrecf  38092  climaddf  38099  mullimc  38100  neglimc  38132  addlimc  38133  0ellimcdiv  38134  dvnmptdivc  38232  dvmptfprod  38239  dvnprodlem1  38240  stoweidlem18  38314  stoweidlem31  38328  stoweidlem55  38352  stoweidlem59  38356  sge0f1o  38670  sge0iunmpt  38706  sge0reuz  38735  iundjiun  38748  hoicvrrex  38841  ovnhoilem1  38886  ovnlecvr2  38895  opnvonmbllem1  38917  vonioo  38968  vonicc  38971  ovmpt2rdxf  41310