Theorem nfeq 2991

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

Syntax hints:   = wceq 1533  ⊤wtru 1534  Ⅎwnf 1780  Ⅎwnfc 2961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-cleq 2814  df-nfc 2963

This theorem is referenced by:  nfeq1  2993  nfeq2  2995  nfne  3119  raleqf  3397  rexeqf  3398  reueq1f  3399  rmoeq1f  3400  rabeqf  3481  csbhypf  3910  sbceqg  4360  nffn  6446  nffo  6583  fvmptd3f  6777  mpteqb  6781  fvmptf  6783  eqfnfv2f  6800  dff13f  7008  ovmpos  7292  ov2gf  7293  ovmpodxf  7294  ovmpodf  7300  eqerlem  8317  seqof2  13422  sumeq2ii  15044  sumss  15075  fsumadd  15090  fsummulc2  15133  fsumrelem  15156  prodeq1f  15256  prodeq2ii  15261  fprodmul  15308  fproddiv  15309  txcnp  22222  ptcnplem  22223  cnmpt11  22265  cnmpt21  22273  cnmptcom  22280  mbfeqalem1  24236  mbflim  24263  itgeq1f  24366  itgeqa  24408  dvmptfsum  24566  ulmss  24979  leibpi  25514  o1cxp  25546  lgseisenlem2  25946  aciunf1lem  30401  sigapildsys  31416  bnj1316  32087  bnj1446  32312  bnj1447  32313  bnj1448  32314  bnj1519  32332  bnj1520  32333  bnj1529  32337  nosupbnd1  33209  subtr  33657  subtr2  33658  bj-sbeqALT  34212  poimirlem25  34911  iuneq2f  35428  mpobi123f  35434  mptbi12f  35438  dvdsrabdioph  39400  fphpd  39406  fvelrnbf  41268  refsum2cnlem1  41287  elrnmpt1sf  41443  disjinfi  41447  choicefi  41456  axccdom  41480  uzublem  41697  fsumf1of  41848  fmuldfeq  41857  mccl  41872  climmulf  41878  climexp  41879  climsuse  41882  climrecf  41883  climaddf  41889  mullimc  41890  neglimc  41921  addlimc  41922  0ellimcdiv  41923  climeldmeqmpt  41942  climfveqmpt  41945  climfveqf  41954  climfveqmpt3  41956  climeldmeqf  41957  climeqf  41962  climeldmeqmpt3  41963  limsupubuzlem  41986  limsupequz  41997  dvnmptdivc  42216  dvmptfprod  42223  dvnprodlem1  42224  stoweidlem18  42297  stoweidlem31  42310  stoweidlem55  42334  stoweidlem59  42338  sge0f1o  42658  sge0iunmpt  42694  sge0reuz  42723  iundjiun  42736  hoicvrrex  42832  ovnhoilem1  42877  ovnlecvr2  42886  opnvonmbllem1  42908  vonioo  42958  vonicc  42961  sssmf  43009  smflim  43047  smfpimcclem  43075  smfpimcc  43076  ovmpordxf  44381