Metamath Proof Explorer

Table of Contents - 2.1.12. Subclasses and subsets

  1. df-ss
  2. dfss
  3. df-pss
  4. dfss2
  5. dfss3
  6. dfss6
  7. dfss2f
  8. dfss3f
  9. nfss
  10. ssel
  11. ssel2
  12. sseli
  13. sselii
  14. sseldi
  15. sseld
  16. sselda
  17. sseldd
  18. ssneld
  19. ssneldd
  20. ssriv
  21. ssrd
  22. ssrdv
  23. sstr2
  24. sstr
  25. sstri
  26. sstrd
  27. sstrid
  28. sstrdi
  29. sylan9ss
  30. sylan9ssr
  31. eqss
  32. eqssi
  33. eqssd
  34. sssseq
  35. eqrd
  36. eqri
  37. eqelssd
  38. ssid
  39. ssidd
  40. ssv
  41. sseq1
  42. sseq2
  43. sseq12
  44. sseq1i
  45. sseq2i
  46. sseq12i
  47. sseq1d
  48. sseq2d
  49. sseq12d
  50. eqsstri
  51. eqsstrri
  52. sseqtri
  53. sseqtrri
  54. eqsstrd
  55. eqsstrrd
  56. sseqtrd
  57. sseqtrrd
  58. 3sstr3i
  59. 3sstr4i
  60. 3sstr3g
  61. 3sstr4g
  62. 3sstr3d
  63. 3sstr4d
  64. eqsstrid
  65. eqsstrrid
  66. sseqtrdi
  67. sseqtrrdi
  68. sseqtrid
  69. sseqtrrid
  70. eqsstrdi
  71. eqsstrrdi
  72. eqimss
  73. eqimss2
  74. eqimssi
  75. eqimss2i
  76. nssne1
  77. nssne2
  78. nss
  79. nelss
  80. ssrexf
  81. ssrmof
  82. ssralv
  83. ssrexv
  84. ss2ralv
  85. ss2rexv
  86. ralss
  87. rexss
  88. ss2ab
  89. abss
  90. ssab
  91. ssabral
  92. ss2abi
  93. ss2abdv
  94. abssdv
  95. abssi
  96. ss2rab
  97. rabss
  98. ssrab
  99. ssrabdv
  100. rabssdv
  101. ss2rabdv
  102. ss2rabi
  103. rabss2
  104. ssab2
  105. ssrab2
  106. ssrab3
  107. rabssrabd
  108. ssrabeq
  109. rabssab
  110. uniiunlem
  111. dfpss2
  112. dfpss3
  113. psseq1
  114. psseq2
  115. psseq1i
  116. psseq2i
  117. psseq12i
  118. psseq1d
  119. psseq2d
  120. psseq12d
  121. pssss
  122. pssne
  123. pssssd
  124. pssned
  125. sspss
  126. pssirr
  127. pssn2lp
  128. sspsstri
  129. ssnpss
  130. psstr
  131. sspsstr
  132. psssstr
  133. psstrd
  134. sspsstrd
  135. psssstrd
  136. npss
  137. ssnelpss
  138. ssnelpssd
  139. ssexnelpss