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. sbciegf
  41. sbcieg
  42. sbciegOLD
  43. sbcie2g
  44. sbcie
  45. sbciedf
  46. sbcied
  47. sbciedOLD
  48. sbcied2
  49. elrabsf
  50. eqsbc1
  51. sbcng
  52. sbcimg
  53. sbcan
  54. sbcor
  55. sbcbig
  56. sbcn1
  57. sbcim1
  58. sbcim1OLD
  59. sbcbid
  60. sbcbidv
  61. sbcbidvOLD
  62. sbcbii
  63. sbcbi1
  64. sbcbi2
  65. sbcbi2OLD
  66. sbcal
  67. sbcex2
  68. sbceqal
  69. sbceqalOLD
  70. sbeqalb
  71. eqsbc2
  72. sbc3an
  73. sbcel1v
  74. sbcel2gv
  75. sbcel21v
  76. sbcimdv
  77. sbcimdvOLD
  78. sbctt
  79. sbcgf
  80. sbc19.21g
  81. sbcg
  82. sbcgOLD
  83. sbcgfi
  84. sbc2iegf
  85. sbc2ie
  86. sbc2ieOLD
  87. sbc2iedv
  88. sbc3ie
  89. sbccomlem
  90. sbccom
  91. sbcralt
  92. sbcrext
  93. sbcralg
  94. sbcrex
  95. sbcreu
  96. reu8nf
  97. sbcabel
  98. rspsbc
  99. rspsbca
  100. rspesbca
  101. spesbc
  102. spesbcd
  103. sbcth2
  104. ra4v
  105. ra4
  106. rmo2
  107. rmo2i
  108. rmo3
  109. rmob
  110. rmoi
  111. rmob2
  112. rmoi2
  113. rmoanim
  114. rmoanimALT
  115. reuan
  116. 2reu1
  117. 2reu2