Theorem nfeq 2913

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

Syntax hints:   = wceq 1542  ⊤wtru 1543  Ⅎwnf 1785  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2729  df-nfc 2886

This theorem is referenced by:  nfeq1  2915  nfeq2  2917  nfne  3034  raleqf  3319  rmoeq1f  3380  rabeqf  3424  csbhypf  3866  sbceqg  4353  nffn  6592  nffo  6746  fvmptd3f  6958  mpteqb  6962  fvmptf  6964  eqfnfv2f  6982  dff13f  7204  ovmpos  7509  ov2gf  7510  ovmpodxf  7511  ovmpodf  7517  eqerlem  8673  seqof2  14016  sumeq2ii  15649  sumss  15680  fsumadd  15696  fsummulc2  15740  fsumrelem  15764  prodeq1f  15865  prodeq2ii  15870  fprodmul  15919  fproddiv  15920  txcnp  23598  ptcnplem  23599  cnmpt11  23641  cnmpt21  23649  cnmptcom  23656  mbfeqalem1  25621  mbflim  25648  itgeq1f  25751  itgeq1fOLD  25752  itgeqa  25794  dvmptfsum  25955  ulmss  26378  leibpi  26922  o1cxp  26955  lgseisenlem2  27356  nosupbnd1  27695  2ndresdju  32740  aciunf1lem  32753  deg1prod  33661  sigapildsys  34325  bnj1316  34981  bnj1446  35206  bnj1447  35207  bnj1448  35208  bnj1519  35226  bnj1520  35227  bnj1529  35231  subtr  36515  subtr2  36516  bj-sbeqALT  37226  poimirlem25  37983  iuneq2f  38494  mpobi123f  38500  mptbi12f  38504  dvdsrabdioph  43259  fphpd  43265  mnringmulrcld  44676  fvelrnbf  45470  refsum2cnlem1  45489  elrnmpt1sf  45640  choicefi  45650  axccdom  45672  uzublem  45879  fsumf1of  46025  fmuldfeq  46034  mccl  46049  climmulf  46055  climexp  46056  climsuse  46059  climrecf  46060  climaddf  46066  mullimc  46067  neglimc  46096  addlimc  46097  0ellimcdiv  46098  climeldmeqmpt  46117  climfveqmpt  46120  climfveqf  46129  climfveqmpt3  46131  climeldmeqf  46132  climeqf  46137  climeldmeqmpt3  46138  limsupubuzlem  46161  limsupequz  46172  dvnmptdivc  46387  dvmptfprod  46394  stoweidlem18  46467  stoweidlem31  46480  stoweidlem55  46504  stoweidlem59  46508  sge0iunmpt  46867  sge0reuz  46896  iundjiun  46909  hoicvrrex  47005  ovnhoilem1  47050  ovnlecvr2  47059  opnvonmbllem1  47081  vonioo  47131  vonicc  47134  sssmf  47187  smflim  47226  smfpimcclem  47256  smfpimcc  47257  cfsetsnfsetf  47521  ovmpordxf  48830