Metamath Proof Explorer

Table of Contents - 2.1.9. Proper substitution of classes for sets

  1. wsbc
  2. df-sbc
  3. dfsbcq
  4. dfsbcq2
  5. sbsbc
  6. sbceq1d
  7. sbceq1dd
  8. sbceqbid
  9. sbc8g
  10. sbc2or
  11. sbcex
  12. sbceq1a
  13. sbceq2a
  14. spsbc
  15. spsbcd
  16. sbcth
  17. sbcthdv
  18. sbcid
  19. nfsbc1d
  20. nfsbc1
  21. nfsbc1v
  22. nfsbcdw
  23. nfsbcw
  24. sbccow
  25. nfsbcd
  26. nfsbc
  27. sbcco
  28. sbcco2
  29. sbc5
  30. sbc5ALT
  31. sbc6g
  32. sbc6gOLD
  33. sbc6
  34. sbc7
  35. cbvsbcw
  36. cbvsbcvw
  37. cbvsbc
  38. cbvsbcv
  39. sbciegft
  40. sbciegftOLD
  41. sbciegf
  42. sbcieg
  43. sbciegOLD
  44. sbcie2g
  45. sbcie
  46. sbciedf
  47. sbcied
  48. sbciedOLD
  49. sbcied2
  50. elrabsf
  51. eqsbc1
  52. sbcng
  53. sbcimg
  54. sbcan
  55. sbcor
  56. sbcbig
  57. sbcn1
  58. sbcim1
  59. sbcim1OLD
  60. sbcbid
  61. sbcbidv
  62. sbcbii
  63. sbcbi1
  64. sbcbi2
  65. sbcal
  66. sbcex2
  67. sbceqal
  68. sbceqalOLD
  69. sbeqalb
  70. eqsbc2
  71. sbc3an
  72. sbcel1v
  73. sbcel2gv
  74. sbcel21v
  75. sbcimdv
  76. sbcimdvOLD
  77. sbctt
  78. sbcgf
  79. sbc19.21g
  80. sbcg
  81. sbcgOLD
  82. sbcgfi
  83. sbc2iegf
  84. sbc2ie
  85. sbc2ieOLD
  86. sbc2iedv
  87. sbc3ie
  88. sbccomlem
  89. sbccom
  90. sbcralt
  91. sbcrext
  92. sbcralg
  93. sbcrex
  94. sbcreu
  95. reu8nf
  96. sbcabel
  97. rspsbc
  98. rspsbca
  99. rspesbca
  100. spesbc
  101. spesbcd
  102. sbcth2
  103. ra4v
  104. ra4
  105. rmo2
  106. rmo2i
  107. rmo3
  108. rmob
  109. rmoi
  110. rmob2
  111. rmoi2
  112. rmoanim
  113. rmoanimALT
  114. reuan
  115. 2reu1
  116. 2reu2