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

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

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 2008  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2728  df-nfc 2886

This theorem is referenced by:  nfeq1  2915  nfeq2  2917  nfne  3034  raleqf  3339  rexeqfOLD  3341  rmoeq1f  3408  rabeqf  3456  csbhypf  3907  sbceqg  4392  nffn  6642  nffo  6794  fvmptd3f  7006  mpteqb  7010  fvmptf  7012  eqfnfv2f  7030  dff13f  7253  ovmpos  7560  ov2gf  7561  ovmpodxf  7562  ovmpodf  7568  eqerlem  8759  seqof2  14083  sumeq2ii  15714  sumss  15745  fsumadd  15761  fsummulc2  15805  fsumrelem  15828  prodeq1f  15927  prodeq2ii  15932  fprodmul  15981  fproddiv  15982  txcnp  23563  ptcnplem  23564  cnmpt11  23606  cnmpt21  23614  cnmptcom  23621  mbfeqalem1  25599  mbflim  25626  itgeq1f  25729  itgeq1fOLD  25730  itgeqa  25772  dvmptfsum  25936  ulmss  26363  leibpi  26909  o1cxp  26942  lgseisenlem2  27344  nosupbnd1  27683  2ndresdju  32632  aciunf1lem  32645  sigapildsys  34198  bnj1316  34856  bnj1446  35081  bnj1447  35082  bnj1448  35083  bnj1519  35101  bnj1520  35102  bnj1529  35106  subtr  36337  subtr2  36338  bj-sbeqALT  36923  poimirlem25  37674  iuneq2f  38185  mpobi123f  38191  mptbi12f  38195  dvdsrabdioph  42800  fphpd  42806  mnringmulrcld  44219  fvelrnbf  45009  refsum2cnlem1  45028  elrnmpt1sf  45180  choicefi  45191  axccdom  45213  uzublem  45424  fsumf1of  45570  fmuldfeq  45579  mccl  45594  climmulf  45600  climexp  45601  climsuse  45604  climrecf  45605  climaddf  45611  mullimc  45612  neglimc  45643  addlimc  45644  0ellimcdiv  45645  climeldmeqmpt  45664  climfveqmpt  45667  climfveqf  45676  climfveqmpt3  45678  climeldmeqf  45679  climeqf  45684  climeldmeqmpt3  45685  limsupubuzlem  45708  limsupequz  45719  dvnmptdivc  45934  dvmptfprod  45941  stoweidlem18  46014  stoweidlem31  46027  stoweidlem55  46051  stoweidlem59  46055  sge0iunmpt  46414  sge0reuz  46443  iundjiun  46456  hoicvrrex  46552  ovnhoilem1  46597  ovnlecvr2  46606  opnvonmbllem1  46628  vonioo  46678  vonicc  46681  sssmf  46734  smflim  46773  smfpimcclem  46803  smfpimcc  46804  cfsetsnfsetf  47054  ovmpordxf  48281