Metamath Proof Explorer

Table of Contents - 1.5.3. Axiom scheme ax-12 (Substitution)

  1. ax-12
  2. ax12v
  3. ax12v2
  4. ax12ev2
  5. ax12ev2c
  6. 19.8a
  7. 19.8ad
  8. sp
  9. spi
  10. sps
  11. 2sp
  12. spsd
  13. 19.2g
  14. 19.21bi
  15. 19.21bbi
  16. 19.23bi
  17. nexr
  18. qexmid
  19. nf5r
  20. nf5ri
  21. nf5rd
  22. spimedv
  23. spimefv
  24. nfim1
  25. nfan1
  26. 19.3t
  27. 19.3
  28. 19.9d
  29. 19.9t
  30. 19.9
  31. 19.21t
  32. 19.21
  33. stdpc5
  34. 19.21-2
  35. 19.23t
  36. 19.23
  37. alimd
  38. alrimi
  39. alrimdd
  40. alrimd
  41. eximd
  42. exlimi
  43. exlimd
  44. exlimimdd
  45. exlimdd
  46. nexd
  47. albid
  48. exbid
  49. nfbidf
  50. 19.16
  51. 19.17
  52. 19.27
  53. 19.28
  54. 19.19
  55. 19.36
  56. 19.36i
  57. 19.37
  58. 19.32
  59. 19.31
  60. 19.41
  61. 19.42
  62. 19.44
  63. 19.45
  64. spimfv
  65. chvarfv
  66. cbv3v2
  67. sbalex
  68. sb4av
  69. sbimd
  70. sbbid
  71. 2sbbid
  72. sbequ1
  73. sbequ2
  74. stdpc7
  75. sbequ12
  76. sbequ12r
  77. sbelx
  78. sbequ12a
  79. sbid
  80. sbcov
  81. sb6a
  82. sbid2vw
  83. axc16g
  84. axc16
  85. axc16gb
  86. axc16nf
  87. axc11v
  88. axc11rv
  89. drsb2
  90. equsalv
  91. equsexv
  92. sbft
  93. sbf
  94. sbf2
  95. sbh
  96. hbs1
  97. nfs1f
  98. sb5
  99. equs5av
  100. 2sb5
  101. dfsb7
  102. sbn
  103. sbex
  104. nf5
  105. nf6
  106. nf5d
  107. nf5di
  108. 19.9h
  109. 19.21h
  110. 19.23h
  111. exlimih
  112. exlimdh
  113. equsalhw
  114. equsexhv
  115. hba1
  116. hbnt
  117. hbn
  118. hbnd
  119. hbim1
  120. hbimd
  121. hbim
  122. hban
  123. hb3an
  124. sbi2
  125. sbim
  126. sbrim
  127. sblim
  128. sbor
  129. sbbi
  130. sblbis
  131. sbrbis
  132. sbrbif
  133. sbnf
  134. sbiev
  135. sbiedw
  136. axc7
  137. axc7e
  138. modal-b
  139. 19.9ht
  140. axc4
  141. axc4i
  142. nfal
  143. nfex
  144. hbex
  145. nfnf
  146. 19.12
  147. nfald
  148. nfexd
  149. nfsbv
  150. sbco2v
  151. aaan
  152. eeor
  153. cbv3v
  154. cbv1v
  155. cbv2w
  156. cbvaldw
  157. cbvexdw
  158. cbv3hv
  159. cbvalv1
  160. cbvexv1
  161. cbval2v
  162. cbvex2v
  163. dvelimhw
  164. pm11.53
  165. 19.12vv
  166. eean
  167. eeanv
  168. eeeanv
  169. ee4anv
  170. ee4anvOLD
  171. sb8v
  172. sb8f
  173. sb8ef
  174. 2sb8ef
  175. sb6rfv
  176. sbnf2
  177. exsb
  178. 2exsb
  179. sbbib
  180. sbbibvv
  181. cbvsbvf
  182. cleljustALT
  183. cleljustALT2
  184. equs5aALT
  185. equs5eALT
  186. axc11r
  187. dral1v
  188. drex1v
  189. drnf1v