Metamath Proof Explorer

Table of Contents - 2.1.14. The empty set

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