Theorem nfeq 2905

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

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

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 2701

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 2721  df-nfc 2878

This theorem is referenced by:  nfeq1  2907  nfeq2  2909  nfne  3026  raleqf  3318  rexeqfOLD  3320  rmoeq1f  3384  rabeqf  3429  csbhypf  3879  sbceqg  4363  nffn  6581  nffo  6735  fvmptd3f  6945  mpteqb  6949  fvmptf  6951  eqfnfv2f  6969  dff13f  7192  ovmpos  7497  ov2gf  7498  ovmpodxf  7499  ovmpodf  7505  eqerlem  8660  seqof2  13967  sumeq2ii  15600  sumss  15631  fsumadd  15647  fsummulc2  15691  fsumrelem  15714  prodeq1f  15813  prodeq2ii  15818  fprodmul  15867  fproddiv  15868  txcnp  23505  ptcnplem  23506  cnmpt11  23548  cnmpt21  23556  cnmptcom  23563  mbfeqalem1  25540  mbflim  25567  itgeq1f  25670  itgeq1fOLD  25671  itgeqa  25713  dvmptfsum  25877  ulmss  26304  leibpi  26850  o1cxp  26883  lgseisenlem2  27285  nosupbnd1  27624  2ndresdju  32600  aciunf1lem  32613  sigapildsys  34145  bnj1316  34803  bnj1446  35028  bnj1447  35029  bnj1448  35030  bnj1519  35048  bnj1520  35049  bnj1529  35053  subtr  36308  subtr2  36309  bj-sbeqALT  36894  poimirlem25  37645  iuneq2f  38156  mpobi123f  38162  mptbi12f  38166  dvdsrabdioph  42803  fphpd  42809  mnringmulrcld  44221  fvelrnbf  45016  refsum2cnlem1  45035  elrnmpt1sf  45187  choicefi  45198  axccdom  45220  uzublem  45429  fsumf1of  45575  fmuldfeq  45584  mccl  45599  climmulf  45605  climexp  45606  climsuse  45609  climrecf  45610  climaddf  45616  mullimc  45617  neglimc  45648  addlimc  45649  0ellimcdiv  45650  climeldmeqmpt  45669  climfveqmpt  45672  climfveqf  45681  climfveqmpt3  45683  climeldmeqf  45684  climeqf  45689  climeldmeqmpt3  45690  limsupubuzlem  45713  limsupequz  45724  dvnmptdivc  45939  dvmptfprod  45946  stoweidlem18  46019  stoweidlem31  46032  stoweidlem55  46056  stoweidlem59  46060  sge0iunmpt  46419  sge0reuz  46448  iundjiun  46461  hoicvrrex  46557  ovnhoilem1  46602  ovnlecvr2  46611  opnvonmbllem1  46633  vonioo  46683  vonicc  46686  sssmf  46739  smflim  46778  smfpimcclem  46808  smfpimcc  46809  cfsetsnfsetf  47062  ovmpordxf  48343