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