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  3326  rexeqfOLD  3328  rmoeq1f  3392  rabeqf  3437  csbhypf  3887  sbceqg  4371  nffn  6599  nffo  6753  fvmptd3f  6965  mpteqb  6969  fvmptf  6971  eqfnfv2f  6989  dff13f  7212  ovmpos  7517  ov2gf  7518  ovmpodxf  7519  ovmpodf  7525  eqerlem  8683  seqof2  14001  sumeq2ii  15635  sumss  15666  fsumadd  15682  fsummulc2  15726  fsumrelem  15749  prodeq1f  15848  prodeq2ii  15853  fprodmul  15902  fproddiv  15903  txcnp  23483  ptcnplem  23484  cnmpt11  23526  cnmpt21  23534  cnmptcom  23541  mbfeqalem1  25518  mbflim  25545  itgeq1f  25648  itgeq1fOLD  25649  itgeqa  25691  dvmptfsum  25855  ulmss  26282  leibpi  26828  o1cxp  26861  lgseisenlem2  27263  nosupbnd1  27602  2ndresdju  32546  aciunf1lem  32559  sigapildsys  34125  bnj1316  34783  bnj1446  35008  bnj1447  35009  bnj1448  35010  bnj1519  35028  bnj1520  35029  bnj1529  35033  subtr  36275  subtr2  36276  bj-sbeqALT  36861  poimirlem25  37612  iuneq2f  38123  mpobi123f  38129  mptbi12f  38133  dvdsrabdioph  42771  fphpd  42777  mnringmulrcld  44190  fvelrnbf  44985  refsum2cnlem1  45004  elrnmpt1sf  45156  choicefi  45167  axccdom  45189  uzublem  45399  fsumf1of  45545  fmuldfeq  45554  mccl  45569  climmulf  45575  climexp  45576  climsuse  45579  climrecf  45580  climaddf  45586  mullimc  45587  neglimc  45618  addlimc  45619  0ellimcdiv  45620  climeldmeqmpt  45639  climfveqmpt  45642  climfveqf  45651  climfveqmpt3  45653  climeldmeqf  45654  climeqf  45659  climeldmeqmpt3  45660  limsupubuzlem  45683  limsupequz  45694  dvnmptdivc  45909  dvmptfprod  45916  stoweidlem18  45989  stoweidlem31  46002  stoweidlem55  46026  stoweidlem59  46030  sge0iunmpt  46389  sge0reuz  46418  iundjiun  46431  hoicvrrex  46527  ovnhoilem1  46572  ovnlecvr2  46581  opnvonmbllem1  46603  vonioo  46653  vonicc  46656  sssmf  46709  smflim  46748  smfpimcclem  46778  smfpimcc  46779  cfsetsnfsetf  47032  ovmpordxf  48300