Theorem nfeq 2762

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 2758	. 2 ⊢ (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
6	5	trud 1484	1 ⊢ Ⅎ𝑥 𝐴 = 𝐵

Syntax hints:   = wceq 1475  ⊤wtru 1476  Ⅎwnf 1699  Ⅎwnfc 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-cleq 2603  df-nfc 2740

This theorem is referenced by:  nfeq1  2764  nfeq2  2766  nfne  2882  raleqf  3111  rexeqf  3112  reueq1f  3113  rmoeq1f  3114  rabeqf  3165  csbhypf  3518  sbceqg  3936  nffn  5901  nffo  6027  fvmptdf  6204  mpteqb  6207  fvmptf  6209  eqfnfv2f  6223  dff13f  6417  ovmpt2s  6682  ov2gf  6683  ovmpt2dxf  6684  ovmpt2df  6690  eqerlem  7663  seqof2  12721  sumeq2ii  14271  sumss  14302  fsumadd  14317  fsummulc2  14358  fsumrelem  14380  prodeq1f  14477  prodeq2ii  14482  fprodmul  14529  fproddiv  14530  fprodle  14566  txcnp  21233  ptcnplem  21234  cnmpt11  21276  cnmpt21  21284  cnmptcom  21291  mbfeqalem  23215  mbflim  23241  itgeq1f  23344  itgeqa  23386  dvmptfsum  23542  ulmss  23955  leibpi  24469  o1cxp  24501  lgseisenlem2  24901  fmptcof2  28839  aciunf1lem  28844  sigapildsys  29552  bnj1316  30145  bnj1446  30367  bnj1447  30368  bnj1448  30369  bnj1519  30387  bnj1520  30388  bnj1529  30392  subtr  31478  subtr2  31479  bj-sbeqALT  32087  poimirlem25  32604  iuneq2f  33133  mpt2bi123f  33141  mptbi12f  33145  dvdsrabdioph  36392  fphpd  36398  fvelrnbf  38200  refsum2cnlem1  38219  dffo3f  38359  elrnmptf  38362  disjrnmpt2  38370  disjinfi  38375  choicefi  38387  axccdom  38411  fsumf1of  38641  fmuldfeq  38650  mccl  38665  climmulf  38671  climexp  38672  climsuse  38675  climrecf  38676  climaddf  38682  mullimc  38683  neglimc  38714  addlimc  38715  0ellimcdiv  38716  climeldmeqmpt  38735  climfveqmpt  38738  dvnmptdivc  38828  dvmptfprod  38835  dvnprodlem1  38836  stoweidlem18  38911  stoweidlem31  38924  stoweidlem55  38948  stoweidlem59  38952  sge0f1o  39275  sge0iunmpt  39311  sge0reuz  39340  iundjiun  39353  hoicvrrex  39446  ovnhoilem1  39491  ovnlecvr2  39500  opnvonmbllem1  39522  vonioo  39573  vonicc  39576  sssmf  39625  smflim  39663  ovmpt2rdxf  41910