Theorem nfeq 2919

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

Syntax hints:   = wceq 1540  ⊤wtru 1541  Ⅎwnf 1783  Ⅎwnfc 2890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2729  df-nfc 2892

This theorem is referenced by:  nfeq1  2921  nfeq2  2923  nfne  3043  raleqf  3353  rexeqfOLD  3355  rmoeq1f  3424  rabeqf  3472  csbhypf  3927  sbceqg  4412  nffn  6667  nffo  6819  fvmptd3f  7031  mpteqb  7035  fvmptf  7037  eqfnfv2f  7055  dff13f  7276  ovmpos  7581  ov2gf  7582  ovmpodxf  7583  ovmpodf  7589  eqerlem  8780  seqof2  14101  sumeq2ii  15729  sumss  15760  fsumadd  15776  fsummulc2  15820  fsumrelem  15843  prodeq1f  15942  prodeq2ii  15947  fprodmul  15996  fproddiv  15997  txcnp  23628  ptcnplem  23629  cnmpt11  23671  cnmpt21  23679  cnmptcom  23686  mbfeqalem1  25676  mbflim  25703  itgeq1f  25806  itgeq1fOLD  25807  itgeqa  25849  dvmptfsum  26013  ulmss  26440  leibpi  26985  o1cxp  27018  lgseisenlem2  27420  nosupbnd1  27759  2ndresdju  32659  aciunf1lem  32672  sigapildsys  34163  bnj1316  34834  bnj1446  35059  bnj1447  35060  bnj1448  35061  bnj1519  35079  bnj1520  35080  bnj1529  35084  subtr  36315  subtr2  36316  bj-sbeqALT  36901  poimirlem25  37652  iuneq2f  38163  mpobi123f  38169  mptbi12f  38173  dvdsrabdioph  42821  fphpd  42827  mnringmulrcld  44247  fvelrnbf  45023  refsum2cnlem1  45042  elrnmpt1sf  45194  choicefi  45205  axccdom  45227  uzublem  45441  fsumf1of  45589  fmuldfeq  45598  mccl  45613  climmulf  45619  climexp  45620  climsuse  45623  climrecf  45624  climaddf  45630  mullimc  45631  neglimc  45662  addlimc  45663  0ellimcdiv  45664  climeldmeqmpt  45683  climfveqmpt  45686  climfveqf  45695  climfveqmpt3  45697  climeldmeqf  45698  climeqf  45703  climeldmeqmpt3  45704  limsupubuzlem  45727  limsupequz  45738  dvnmptdivc  45953  dvmptfprod  45960  stoweidlem18  46033  stoweidlem31  46046  stoweidlem55  46070  stoweidlem59  46074  sge0iunmpt  46433  sge0reuz  46462  iundjiun  46475  hoicvrrex  46571  ovnhoilem1  46616  ovnlecvr2  46625  opnvonmbllem1  46647  vonioo  46697  vonicc  46700  sssmf  46753  smflim  46792  smfpimcclem  46822  smfpimcc  46823  cfsetsnfsetf  47070  ovmpordxf  48255