Theorem nfeq 2939

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

This proof depends on syntax axioms:   = wceq 1570  ⊤wtru 1571  Ⅎwnf 1816  Ⅎwnfc 2911

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-cleq 2755  df-nfc 2913

This theorem is used by:  nfeq1  2941  nfeq2  2943  nfne  3062  raleqf  3345  rmoeq1f  3406  rabeqf  3449  csbhypf  3879  sbceqg  4373  nffn  6668  nffo  6825  fvmptd3f  7040  mpteqb  7044  fvmptf  7046  eqfnfv2f  7064  dff13f  7290  ovmpos  7600  ov2gf  7601  ovmpodxf  7602  ovmpodf  7608  eqerlem  8791  seqof2  14243  sumeq2ii  15904  sumss  15934  fsumadd  15950  fsummulc2  15994  fsumrelem  16018  prodeq1f  16119  prodeq2ii  16124  fprodmul  16171  fproddiv  16172  txcnp  23994  ptcnplem  23995  cnmpt11  24037  cnmpt21  24045  cnmptcom  24052  mbfeqalem1  26017  mbflim  26044  itgeq1f  26147  itgeqa  26189  dvmptfsum  26350  ulmss  26781  leibpi  27327  o1cxp  27359  lgseisenlem2  27760  nosupbnd1  28128  2ndresdju  33341  aciunf1lem  33354  deg1prod  34218  sigapildsys  34906  bnj1316  35561  bnj1446  35786  bnj1447  35787  bnj1448  35788  bnj1519  35806  bnj1520  35807  bnj1529  35811  subtr  37317  subtr2  37318  bj-sbeqALT  38027  poimirlem25  38831  iuneq2f  39354  mpobi123f  39360  mptbi12f  39364  dvdsrabdioph  44083  fphpd  44089  mnringmulrcld  45487  fvelrnbf  46309  refsum2cnlem1  46328  elrnmpt1sf  46477  choicefi  46487  axccdom  46508  uzublem  46713  fsumf1of  46859  fmuldfeq  46868  mccl  46883  climmulf  46889  climexp  46890  climsuse  46893  climrecf  46894  climaddf  46900  mullimc  46901  neglimc  46930  addlimc  46931  0ellimcdiv  46932  climeldmeqmpt  46951  climfveqmpt  46954  climfveqf  46963  climfveqmpt3  46965  climeldmeqf  46966  climeqf  46971  climeldmeqmpt3  46972  limsupubuzlem  46995  limsupequz  47006  dvnmptdivc  47221  dvmptfprod  47228  stoweidlem18  47301  stoweidlem31  47314  stoweidlem55  47338  stoweidlem59  47342  sge0iunmpt  47701  sge0reuz  47730  iundjiun  47743  hoicvrrex  47839  ovnhoilem1  47884  ovnlecvr2  47893  opnvonmbllem1  47915  vonioo  47965  vonicc  47968  smflim  48060  smfpimcclem  48090  smfpimcc  48091  cfsetsnfsetf  48401  ovmpordxf  49782