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