Theorem nfeq 2935

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

This proof depends on syntax axioms:   = wceq 1569  ⊤wtru 1570  Ⅎwnf 1815  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-cleq 2752  df-nfc 2909

This theorem is used by:  nfeq1  2937  nfeq2  2939  nfne  3058  raleqf  3341  rmoeq1f  3402  rabeqf  3445  csbhypf  3875  sbceqg  4369  nffn  6643  nffo  6800  fvmptd3f  7014  mpteqb  7018  fvmptf  7020  eqfnfv2f  7038  dff13f  7263  ovmpos  7572  ov2gf  7573  ovmpodxf  7574  ovmpodf  7580  eqerlem  8760  seqof2  14210  sumeq2ii  15869  sumss  15899  fsumadd  15915  fsummulc2  15959  fsumrelem  15983  prodeq1f  16084  prodeq2ii  16089  fprodmul  16136  fproddiv  16137  txcnp  23948  ptcnplem  23949  cnmpt11  23991  cnmpt21  23999  cnmptcom  24006  mbfeqalem1  25971  mbflim  25998  itgeq1f  26101  itgeqa  26143  dvmptfsum  26304  ulmss  26733  leibpi  27279  o1cxp  27311  lgseisenlem2  27712  nosupbnd1  28080  2ndresdju  33294  aciunf1lem  33307  deg1prod  34165  sigapildsys  34845  bnj1316  35500  bnj1446  35725  bnj1447  35726  bnj1448  35727  bnj1519  35745  bnj1520  35746  bnj1529  35750  subtr  37198  subtr2  37199  bj-sbeqALT  37908  poimirlem25  38672  iuneq2f  39197  mpobi123f  39203  mptbi12f  39207  dvdsrabdioph  43926  fphpd  43932  mnringmulrcld  45335  fvelrnbf  46143  refsum2cnlem1  46162  elrnmpt1sf  46312  choicefi  46322  axccdom  46343  uzublem  46548  fsumf1of  46694  fmuldfeq  46703  mccl  46718  climmulf  46724  climexp  46725  climsuse  46728  climrecf  46729  climaddf  46735  mullimc  46736  neglimc  46765  addlimc  46766  0ellimcdiv  46767  climeldmeqmpt  46786  climfveqmpt  46789  climfveqf  46798  climfveqmpt3  46800  climeldmeqf  46801  climeqf  46806  climeldmeqmpt3  46807  limsupubuzlem  46830  limsupequz  46841  dvnmptdivc  47056  dvmptfprod  47063  stoweidlem18  47136  stoweidlem31  47149  stoweidlem55  47173  stoweidlem59  47177  sge0iunmpt  47536  sge0reuz  47565  iundjiun  47578  hoicvrrex  47674  ovnhoilem1  47719  ovnlecvr2  47728  opnvonmbllem1  47750  vonioo  47800  vonicc  47803  smflim  47895  smfpimcclem  47925  smfpimcc  47926  cfsetsnfsetf  48236  ovmpordxf  49559