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  32592  aciunf1lem  32605  sigapildsys  34129  bnj1316  34787  bnj1446  35012  bnj1447  35013  bnj1448  35014  bnj1519  35032  bnj1520  35033  bnj1529  35037  subtr  36288  subtr2  36289  bj-sbeqALT  36874  poimirlem25  37625  iuneq2f  38136  mpobi123f  38142  mptbi12f  38146  dvdsrabdioph  42783  fphpd  42789  mnringmulrcld  44201  fvelrnbf  44996  refsum2cnlem1  45015  elrnmpt1sf  45167  choicefi  45178  axccdom  45200  uzublem  45409  fsumf1of  45555  fmuldfeq  45564  mccl  45579  climmulf  45585  climexp  45586  climsuse  45589  climrecf  45590  climaddf  45596  mullimc  45597  neglimc  45628  addlimc  45629  0ellimcdiv  45630  climeldmeqmpt  45649  climfveqmpt  45652  climfveqf  45661  climfveqmpt3  45663  climeldmeqf  45664  climeqf  45669  climeldmeqmpt3  45670  limsupubuzlem  45693  limsupequz  45704  dvnmptdivc  45919  dvmptfprod  45926  stoweidlem18  45999  stoweidlem31  46012  stoweidlem55  46036  stoweidlem59  46040  sge0iunmpt  46399  sge0reuz  46428  iundjiun  46441  hoicvrrex  46537  ovnhoilem1  46582  ovnlecvr2  46591  opnvonmbllem1  46613  vonioo  46663  vonicc  46666  sssmf  46719  smflim  46758  smfpimcclem  46788  smfpimcc  46789  cfsetsnfsetf  47042  ovmpordxf  48323