Theorem nfeq 2912

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

Syntax hints:   = wceq 1541  ⊤wtru 1542  Ⅎwnf 1784  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2728  df-nfc 2885

This theorem is referenced by:  nfeq1  2914  nfeq2  2916  nfne  3033  raleqf  3325  rexeqfOLD  3327  rmoeq1f  3389  rabeqf  3433  csbhypf  3877  sbceqg  4364  nffn  6591  nffo  6745  fvmptd3f  6956  mpteqb  6960  fvmptf  6962  eqfnfv2f  6980  dff13f  7201  ovmpos  7506  ov2gf  7507  ovmpodxf  7508  ovmpodf  7514  eqerlem  8670  seqof2  13983  sumeq2ii  15616  sumss  15647  fsumadd  15663  fsummulc2  15707  fsumrelem  15730  prodeq1f  15829  prodeq2ii  15834  fprodmul  15883  fproddiv  15884  txcnp  23564  ptcnplem  23565  cnmpt11  23607  cnmpt21  23615  cnmptcom  23622  mbfeqalem1  25598  mbflim  25625  itgeq1f  25728  itgeq1fOLD  25729  itgeqa  25771  dvmptfsum  25935  ulmss  26362  leibpi  26908  o1cxp  26941  lgseisenlem2  27343  nosupbnd1  27682  2ndresdju  32727  aciunf1lem  32740  deg1prod  33664  sigapildsys  34319  bnj1316  34976  bnj1446  35201  bnj1447  35202  bnj1448  35203  bnj1519  35221  bnj1520  35222  bnj1529  35226  subtr  36508  subtr2  36509  bj-sbeqALT  37101  poimirlem25  37846  iuneq2f  38357  mpobi123f  38363  mptbi12f  38367  dvdsrabdioph  43052  fphpd  43058  mnringmulrcld  44469  fvelrnbf  45263  refsum2cnlem1  45282  elrnmpt1sf  45433  choicefi  45444  axccdom  45466  uzublem  45674  fsumf1of  45820  fmuldfeq  45829  mccl  45844  climmulf  45850  climexp  45851  climsuse  45854  climrecf  45855  climaddf  45861  mullimc  45862  neglimc  45891  addlimc  45892  0ellimcdiv  45893  climeldmeqmpt  45912  climfveqmpt  45915  climfveqf  45924  climfveqmpt3  45926  climeldmeqf  45927  climeqf  45932  climeldmeqmpt3  45933  limsupubuzlem  45956  limsupequz  45967  dvnmptdivc  46182  dvmptfprod  46189  stoweidlem18  46262  stoweidlem31  46275  stoweidlem55  46299  stoweidlem59  46303  sge0iunmpt  46662  sge0reuz  46691  iundjiun  46704  hoicvrrex  46800  ovnhoilem1  46845  ovnlecvr2  46854  opnvonmbllem1  46876  vonioo  46926  vonicc  46929  sssmf  46982  smflim  47021  smfpimcclem  47051  smfpimcc  47052  cfsetsnfsetf  47304  ovmpordxf  48585