Metamath Proof Explorer


Table of Contents - 2.1.14. The empty set

  1. c0
  2. df-nul
  3. dfnul2
  4. dfnul3
  5. noel
  6. nel02
  7. n0i
  8. ne0i
  9. ne0d
  10. n0ii
  11. ne0ii
  12. vn0
  13. eq0f
  14. neq0f
  15. n0f
  16. eq0
  17. neq0
  18. n0
  19. eq0OLD
  20. neq0OLD
  21. n0OLD
  22. nel0
  23. reximdva0
  24. rspn0
  25. rspn0OLD
  26. n0rex
  27. ssn0rex
  28. n0moeu
  29. rex0
  30. reu0
  31. rmo0
  32. 0el
  33. n0el
  34. eqeuel
  35. ssdif0
  36. difn0
  37. pssdifn0
  38. pssdif
  39. ndisj
  40. difin0ss
  41. inssdif0
  42. difid
  43. difidALT
  44. dif0
  45. ab0
  46. dfnf5
  47. ab0orv
  48. abn0
  49. rab0
  50. rabeq0
  51. rabn0
  52. rabxm
  53. rabnc
  54. elneldisj
  55. elnelun
  56. un0
  57. in0
  58. 0un
  59. 0in
  60. inv1
  61. unv
  62. 0ss
  63. ss0b
  64. ss0
  65. sseq0
  66. ssn0
  67. 0dif
  68. abf
  69. abfOLD
  70. eq0rdv
  71. csbprc
  72. csb0
  73. csb0OLD
  74. sbcel12
  75. sbceqg
  76. sbceqi
  77. sbcnel12g
  78. sbcne12
  79. sbcel1g
  80. sbceq1g
  81. sbcel2
  82. sbceq2g
  83. csbcom
  84. sbcnestgfw
  85. csbnestgfw
  86. sbcnestgw
  87. csbnestgw
  88. sbcco3gw
  89. sbcnestgf
  90. csbnestgf
  91. sbcnestg
  92. csbnestg
  93. sbcco3g
  94. csbco3g
  95. csbnest1g
  96. csbidm
  97. csbvarg
  98. csbvargi
  99. sbccsb
  100. sbccsb2
  101. rspcsbela
  102. sbnfc2
  103. csbab
  104. csbun
  105. csbin
  106. csbie2df
  107. 2nreu
  108. un00
  109. vss
  110. 0pss
  111. npss0
  112. pssv
  113. disj
  114. disjOLD
  115. disjr
  116. disj1
  117. reldisj
  118. reldisjOLD
  119. disj3
  120. disjne
  121. disjeq0
  122. disjel
  123. disj2
  124. disj4
  125. ssdisj
  126. disjpss
  127. undisj1
  128. undisj2
  129. ssindif0
  130. inelcm
  131. minel
  132. undif4
  133. disjssun
  134. vdif0
  135. difrab0eq
  136. pssnel
  137. disjdif
  138. difin0
  139. unvdif
  140. undif1
  141. undif2
  142. undifabs
  143. inundif
  144. disjdif2
  145. difun2
  146. undif
  147. ssdifin0
  148. ssdifeq0
  149. ssundif
  150. difcom
  151. pssdifcom1
  152. pssdifcom2
  153. difdifdir
  154. uneqdifeq
  155. raldifeq
  156. r19.2z
  157. r19.2zb
  158. r19.3rz
  159. r19.28z
  160. r19.3rzv
  161. r19.9rzv
  162. r19.28zv
  163. r19.37zv
  164. r19.45zv
  165. r19.44zv
  166. r19.27z
  167. r19.27zv
  168. r19.36zv
  169. rzal
  170. rexn0
  171. ralidm
  172. ral0
  173. ralf0
  174. ralnralall
  175. falseral0
  176. raaan
  177. raaanv
  178. sbss
  179. sbcssg
  180. raaan2
  181. 2reu4lem
  182. 2reu4