MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfeq Structured version   Visualization version   GIF version

Theorem nfeq 2666
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
StepHypRef Expression
1 nfnfc.1 . . . 4 𝑥𝐴
21a1i 11 . . 3 (⊤ → 𝑥𝐴)
3 nfeq.2 . . . 4 𝑥𝐵
43a1i 11 . . 3 (⊤ → 𝑥𝐵)
52, 4nfeqd 2662 . 2 (⊤ → Ⅎ𝑥 𝐴 = 𝐵)
65trud 1483 1 𝑥 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wtru 1475  wnf 1698  wnfc 2642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-nf 1699  df-cleq 2507  df-nfc 2644
This theorem is referenced by:  nfeq1  2668  nfeq2  2670  nfne  2786  raleqf  3015  rexeqf  3016  reueq1f  3017  rmoeq1f  3018  rabeqf  3069  csbhypf  3422  sbceqg  3839  nffn  5791  nffo  5916  fvmptdf  6093  mpteqb  6096  fvmptf  6098  eqfnfv2f  6112  dff13f  6299  ovmpt2s  6564  ov2gf  6565  ovmpt2dxf  6566  ovmpt2df  6572  eqerlem  7543  seqof2  12593  sumeq2ii  14144  sumss  14175  fsumadd  14190  fsummulc2  14231  fsumrelem  14253  prodeq1f  14350  prodeq2ii  14355  fprodmul  14402  fproddiv  14403  fprodle  14439  txcnp  21140  ptcnplem  21141  cnmpt11  21183  cnmpt21  21191  cnmptcom  21198  mbfeqalem  23094  mbflim  23120  itgeq1f  23223  itgeqa  23265  dvmptfsum  23421  ulmss  23846  leibpi  24360  o1cxp  24392  lgseisenlem2  24794  fmptcof2  28631  aciunf1lem  28636  sigapildsys  29352  oms0OLD  29496  bnj1316  29994  bnj1446  30216  bnj1447  30217  bnj1448  30218  bnj1519  30236  bnj1520  30237  bnj1529  30241  subtr  31317  subtr2  31318  bj-sbeqALT  31922  poimirlem25  32498  iuneq2f  33027  mpt2bi123f  33035  mptbi12f  33039  dvdsrabdioph  36286  fphpd  36292  fvelrnbf  38101  refsum2cnlem1  38120  dffo3f  38261  elrnmptf  38264  disjrnmpt2  38272  disjinfi  38277  choicefi  38289  axccdom  38313  fsumf1of  38544  fmuldfeq  38553  mccl  38568  climmulf  38574  climexp  38575  climsuse  38578  climrecf  38579  climaddf  38585  mullimc  38586  neglimc  38618  addlimc  38619  0ellimcdiv  38620  climeldmeqmpt  38639  climfveqmpt  38642  dvnmptdivc  38735  dvmptfprod  38742  dvnprodlem1  38743  stoweidlem18  38818  stoweidlem31  38831  stoweidlem55  38855  stoweidlem59  38859  sge0f1o  39186  sge0iunmpt  39222  sge0reuz  39251  iundjiun  39264  hoicvrrex  39357  ovnhoilem1  39402  ovnlecvr2  39411  opnvonmbllem1  39433  vonioo  39484  vonicc  39487  sssmf  39536  smflim  39574  ovmpt2rdxf  42019
  Copyright terms: Public domain W3C validator