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 1577	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

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 2752  df-nfc 2909

This theorem is used by:  nfeq1  2937  nfeq2  2939  nfne  3058  raleqf  3341  rmoeq1f  3402  rabeqf  3445  csbhypf  3875  sbceqg  4370  nffn  6631  nffo  6788  fvmptd3f  7002  mpteqb  7006  fvmptf  7008  eqfnfv2f  7026  dff13f  7252  ovmpos  7561  ov2gf  7562  ovmpodxf  7563  ovmpodf  7569  eqerlem  8732  seqof2  14124  sumeq2ii  15780  sumss  15810  fsumadd  15826  fsummulc2  15870  fsumrelem  15894  prodeq1f  15995  prodeq2ii  16000  fprodmul  16047  fproddiv  16048  txcnp  23846  ptcnplem  23847  cnmpt11  23889  cnmpt21  23897  cnmptcom  23904  mbfeqalem1  25869  mbflim  25896  itgeq1f  25999  itgeqa  26041  dvmptfsum  26202  ulmss  26633  leibpi  27179  o1cxp  27211  lgseisenlem2  27612  nosupbnd1  27950  2ndresdju  33122  aciunf1lem  33135  deg1prod  33993  sigapildsys  34673  bnj1316  35329  bnj1446  35554  bnj1447  35555  bnj1448  35556  bnj1519  35574  bnj1520  35575  bnj1529  35579  subtr  36933  subtr2  36934  bj-sbeqALT  37643  poimirlem25  38394  iuneq2f  38904  mpobi123f  38910  mptbi12f  38914  dvdsrabdioph  43651  fphpd  43657  mnringmulrcld  45066  fvelrnbf  45852  refsum2cnlem1  45871  elrnmpt1sf  46021  choicefi  46031  axccdom  46052  uzublem  46258  fsumf1of  46404  fmuldfeq  46413  mccl  46428  climmulf  46434  climexp  46435  climsuse  46438  climrecf  46439  climaddf  46445  mullimc  46446  neglimc  46475  addlimc  46476  0ellimcdiv  46477  climeldmeqmpt  46496  climfveqmpt  46499  climfveqf  46508  climfveqmpt3  46510  climeldmeqf  46511  climeqf  46516  climeldmeqmpt3  46517  limsupubuzlem  46540  limsupequz  46551  dvnmptdivc  46766  dvmptfprod  46773  stoweidlem18  46846  stoweidlem31  46859  stoweidlem55  46883  stoweidlem59  46887  sge0iunmpt  47246  sge0reuz  47275  iundjiun  47288  hoicvrrex  47384  ovnhoilem1  47429  ovnlecvr2  47438  opnvonmbllem1  47460  vonioo  47510  vonicc  47513  smflim  47605  smfpimcclem  47635  smfpimcc  47636  cfsetsnfsetf  47946  ovmpordxf  49269