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. sbequ1
  73. sbequ2
  74. sbequ2OLD
  75. stdpc7
  76. sbequ12
  77. sbequ12r
  78. sbelx
  79. sbequ12a
  80. sbid
  81. sbcov
  82. sb6a
  83. sbid2vw
  84. axc16g
  85. axc16
  86. axc16gb
  87. axc16nf
  88. axc11v
  89. axc11rv
  90. drsb2
  91. equsalv
  92. equsexv
  93. sbft
  94. sbf
  95. sbf2
  96. sbh
  97. hbs1
  98. nfs1f
  99. sb5
  100. sb56
  101. sb56OLD
  102. equs5av
  103. sb5OLD
  104. 2sb5
  105. sbco4lem
  106. sbco4
  107. dfsb7
  108. dfsb7OLD
  109. sbn
  110. sbex
  111. sbbibOLD
  112. nf5
  113. nf6
  114. nf5d
  115. nf5di
  116. 19.9h
  117. 19.21h
  118. 19.23h
  119. exlimih
  120. exlimdh
  121. equsalhw
  122. equsexhv
  123. hba1
  124. hbnt
  125. hbn
  126. hbnd
  127. hbim1
  128. hbimd
  129. hbim
  130. hban
  131. hb3an
  132. sbi2
  133. sbim
  134. sbanOLD
  135. sbrim
  136. sbrimv
  137. sblim
  138. sbor
  139. sbbi
  140. sblbis
  141. sbrbis
  142. sbrbif
  143. sbi1vOLD
  144. sbimvOLD
  145. sbanvOLD
  146. sbbivOLD
  147. sblbisvOLD
  148. sbiev
  149. sbiedw
  150. sbiedwOLD
  151. axc7
  152. axc7e
  153. modal-b
  154. 19.9ht
  155. axc4
  156. axc4i
  157. nfal
  158. nfex
  159. hbex
  160. nfnf
  161. 19.12
  162. nfald
  163. nfexd
  164. nfsbv
  165. nfsbvOLD
  166. hbsbwOLD
  167. sbco2v
  168. aaan
  169. eeor
  170. cbv3v
  171. cbv1v
  172. cbv2w
  173. cbvaldw
  174. cbvexdw
  175. cbv3hv
  176. cbvalv1
  177. cbvexv1
  178. cbval2v
  179. cbval2vOLD
  180. cbvex2v
  181. dvelimhw
  182. pm11.53
  183. 19.12vv
  184. eean
  185. eeanv
  186. eeeanv
  187. ee4anv
  188. sb8v
  189. sb8ev
  190. 2sb8ev
  191. sb6rfv
  192. sbnf2
  193. exsb
  194. 2exsb
  195. sbbib
  196. sbbibvv
  197. cleljustALT
  198. cleljustALT2
  199. equs5aALT
  200. equs5eALT
  201. axc11r
  202. dral1v
  203. drex1v
  204. drnf1v