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. sbciegftOLD
  40. sbciegf
  41. sbcieg
  42. sbcie2g
  43. sbcie
  44. sbciedf
  45. sbcied
  46. sbcied2
  47. elrabsf
  48. eqsbc1
  49. sbcng
  50. sbcimg
  51. sbcan
  52. sbcor
  53. sbcbig
  54. sbcn1
  55. sbcim1
  56. sbcbid
  57. sbcbidv
  58. sbcbii
  59. sbcbi1
  60. sbcbi2
  61. sbcal
  62. sbcex2
  63. sbceqal
  64. sbeqalb
  65. eqsbc2
  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. sbccomlemOLD
  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