Theorem nfeq 2938

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

Syntax hints:   = wceq 1570  ⊤wtru 1571  Ⅎwnf 1813  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-cleq 2755  df-nfc 2912

This theorem is referenced by:  nfeq1  2940  nfeq2  2942  nfne  3061  raleqf  3345  rmoeq1f  3406  rabeqf  3450  csbhypf  3881  sbceqg  4377  nffn  6634  nffo  6791  fvmptd3f  7005  mpteqb  7009  fvmptf  7011  eqfnfv2f  7029  dff13f  7253  ovmpos  7558  ov2gf  7559  ovmpodxf  7560  ovmpodf  7566  eqerlem  8726  seqof2  14092  sumeq2ii  15740  sumss  15771  fsumadd  15787  fsummulc2  15831  fsumrelem  15855  prodeq1f  15956  prodeq2ii  15961  fprodmul  16010  fproddiv  16011  txcnp  23777  ptcnplem  23778  cnmpt11  23820  cnmpt21  23828  cnmptcom  23835  mbfeqalem1  25800  mbflim  25827  itgeq1f  25930  itgeq1fOLD  25931  itgeqa  25973  dvmptfsum  26134  ulmss  26560  leibpi  27107  o1cxp  27139  lgseisenlem2  27540  nosupbnd1  27878  2ndresdju  32994  aciunf1lem  33007  deg1prod  33873  sigapildsys  34552  bnj1316  35208  bnj1446  35433  bnj1447  35434  bnj1448  35435  bnj1519  35453  bnj1520  35454  bnj1529  35458  subtr  36825  subtr2  36826  bj-sbeqALT  37535  poimirlem25  38296  iuneq2f  38805  mpobi123f  38811  mptbi12f  38815  dvdsrabdioph  43537  fphpd  43543  mnringmulrcld  44952  fvelrnbf  45738  refsum2cnlem1  45757  elrnmpt1sf  45907  choicefi  45917  axccdom  45938  uzublem  46144  fsumf1of  46290  fmuldfeq  46299  mccl  46314  climmulf  46320  climexp  46321  climsuse  46324  climrecf  46325  climaddf  46331  mullimc  46332  neglimc  46361  addlimc  46362  0ellimcdiv  46363  climeldmeqmpt  46382  climfveqmpt  46385  climfveqf  46394  climfveqmpt3  46396  climeldmeqf  46397  climeqf  46402  climeldmeqmpt3  46403  limsupubuzlem  46426  limsupequz  46437  dvnmptdivc  46652  dvmptfprod  46659  stoweidlem18  46732  stoweidlem31  46745  stoweidlem55  46769  stoweidlem59  46773  sge0iunmpt  47132  sge0reuz  47161  iundjiun  47174  hoicvrrex  47270  ovnhoilem1  47315  ovnlecvr2  47324  opnvonmbllem1  47346  vonioo  47396  vonicc  47399  smflim  47491  smfpimcclem  47521  smfpimcc  47522  cfsetsnfsetf  47795  ovmpordxf  49119