Metamath Proof Explorer


Table of Contents - 20.43.6. General auxiliary theorems (2)

  1. Logical conjunction - extension
    1. an4com24
  2. Abbreviated conjunction and disjunction of three wff's - extension
    1. 3an4ancom24
    2. 4an21
  3. Negated membership (alternative)
    1. cnelbr
    2. df-nelbr
    3. dfnelbr2
    4. nelbr
    5. nelbrim
    6. nelbrnel
    7. nelbrnelim
  4. The empty set - extension
    1. ralralimp
  5. Indexed union and intersection - extension
    1. otiunsndisjX
  6. Functions - extension
    1. fvifeq
    2. rnfdmpr
    3. imarnf1pr
    4. funop1
    5. fun2dmnopgexmpl
    6. opabresex0d
    7. opabbrfex0d
    8. opabresexd
    9. opabbrfexd
    10. f1oresf1orab
    11. f1oresf1o
    12. f1oresf1o2
  7. Maps-to notation - extension
    1. fvmptrab
    2. fvmptrabdm
  8. Ordering on reals - extension
    1. leltletr
  9. Subtraction - extension
    1. cnambpcma
    2. cnapbmcpd
    3. addsubeq0
  10. Ordering on reals (cont.) - extension
    1. leaddsuble
    2. 2leaddle2
    3. ltnltne
    4. p1lep2
    5. ltsubsubaddltsub
    6. zm1nn
  11. Imaginary and complex number properties - extension
    1. readdcnnred
    2. resubcnnred
    3. recnmulnred
    4. cndivrenred
    5. sqrtnegnre
  12. Nonnegative integers (as a subset of complex numbers) - extension
    1. nn0resubcl
  13. Integers (as a subset of complex numbers) - extension
    1. zgeltp1eq
  14. Decimal arithmetic - extension
    1. 1t10e1p1e11
    2. deccarry
  15. Upper sets of integers - extension
    1. eluzge0nn0
  16. Infinity and the extended real number system (cont.) - extension
    1. nltle2tri
  17. Finite intervals of integers - extension
    1. ssfz12
    2. elfz2z
    3. 2elfz3nn0
    4. fz0addcom
    5. 2elfz2melfz
    6. fz0addge0
    7. elfzlble
    8. elfzelfzlble
  18. Half-open integer ranges - extension
    1. fzopred
    2. fzopredsuc
    3. 1fzopredsuc
    4. el1fzopredsuc
    5. subsubelfzo0
    6. fzoopth
    7. 2ffzoeq
  19. The modulo (remainder) operation - extension
    1. m1mod0mod1
    2. elmod2
  20. The infinite sequence builder "seq"
    1. smonoord
  21. Finite and infinite sums - extension
    1. fsummsndifre
    2. fsumsplitsndif
    3. fsummmodsndifre
    4. fsummmodsnunz
  22. Extensible structures - extension
    1. setsidel
    2. setsnidel
    3. setsv