Metamath Proof Explorer

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

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