Theorem nfeq 2921

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

Syntax hints:   = wceq 1539  ⊤wtru 1540  Ⅎwnf 1786  Ⅎwnfc 2888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-cleq 2731  df-nfc 2890

This theorem is referenced by:  nfeq1  2923  nfeq2  2925  nfne  3046  raleqf  3333  rexeqf  3334  reueq1f  3335  rmoeq1f  3336  rabeqf  3416  csbhypf  3862  sbceqg  4344  nffn  6541  nffo  6696  fvmptd3f  6899  mpteqb  6903  fvmptf  6905  eqfnfv2f  6922  dff13f  7138  ovmpos  7430  ov2gf  7431  ovmpodxf  7432  ovmpodf  7438  eqerlem  8541  seqof2  13790  sumeq2ii  15414  sumss  15445  fsumadd  15461  fsummulc2  15505  fsumrelem  15528  prodeq1f  15627  prodeq2ii  15632  fprodmul  15679  fproddiv  15680  txcnp  22780  ptcnplem  22781  cnmpt11  22823  cnmpt21  22831  cnmptcom  22838  mbfeqalem1  24814  mbflim  24841  itgeq1f  24945  itgeqa  24987  dvmptfsum  25148  ulmss  25565  leibpi  26101  o1cxp  26133  lgseisenlem2  26533  2ndresdju  30995  aciunf1lem  31008  sigapildsys  32139  bnj1316  32809  bnj1446  33034  bnj1447  33035  bnj1448  33036  bnj1519  33054  bnj1520  33055  bnj1529  33059  nosupbnd1  33926  subtr  34512  subtr2  34513  bj-sbeqALT  35094  poimirlem25  35811  iuneq2f  36323  mpobi123f  36329  mptbi12f  36333  dvdsrabdioph  40639  fphpd  40645  mnringmulrcld  41853  fvelrnbf  42568  refsum2cnlem1  42587  elrnmpt1sf  42734  choicefi  42747  axccdom  42769  uzublem  42977  fsumf1of  43122  fmuldfeq  43131  mccl  43146  climmulf  43152  climexp  43153  climsuse  43156  climrecf  43157  climaddf  43163  mullimc  43164  neglimc  43195  addlimc  43196  0ellimcdiv  43197  climeldmeqmpt  43216  climfveqmpt  43219  climfveqf  43228  climfveqmpt3  43230  climeldmeqf  43231  climeqf  43236  climeldmeqmpt3  43237  limsupubuzlem  43260  limsupequz  43271  dvnmptdivc  43486  dvmptfprod  43493  dvnprodlem1  43494  stoweidlem18  43566  stoweidlem31  43579  stoweidlem55  43603  stoweidlem59  43607  sge0f1o  43927  sge0iunmpt  43963  sge0reuz  43992  iundjiun  44005  hoicvrrex  44101  ovnhoilem1  44146  ovnlecvr2  44155  opnvonmbllem1  44177  vonioo  44227  vonicc  44230  sssmf  44283  smflim  44322  smfpimcclem  44351  smfpimcc  44352  cfsetsnfsetf  44563  ovmpordxf  45685