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. eqsbc1
  48. sbcng
  49. sbcimg
  50. sbcan
  51. sbcor
  52. sbcbig
  53. sbcn1
  54. sbcim1
  55. sbcbid
  56. sbcbidv
  57. sbcbii
  58. sbcbi1
  59. sbcbi2
  60. sbcal
  61. sbcex2
  62. sbceqal
  63. sbeqalb
  64. eqsbc2
  65. sbc3an
  66. sbcel1v
  67. sbcel2gv
  68. sbcel21v
  69. sbcimdv
  70. sbctt
  71. sbcgf
  72. sbc19.21g
  73. sbcg
  74. sbcgfi
  75. sbc2iegf
  76. sbc2ie
  77. sbc2iedv
  78. sbc3ie
  79. sbccomlem
  80. sbccomlemOLD
  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