Metamath Proof Explorer

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

  1. ax-12
  2. ax12v
  3. ax12v2
  4. ax12ev2
  5. 19.8a
  6. 19.8ad
  7. sp
  8. spi
  9. sps
  10. 2sp
  11. spsd
  12. 19.2g
  13. 19.21bi
  14. 19.21bbi
  15. 19.23bi
  16. nexr
  17. qexmid
  18. nf5r
  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. nexd
  46. albid
  47. exbid
  48. nfbidf
  49. 19.16
  50. 19.17
  51. 19.27
  52. 19.28
  53. 19.19
  54. 19.36
  55. 19.36i
  56. 19.37
  57. 19.32
  58. 19.31
  59. 19.41
  60. 19.42
  61. 19.44
  62. 19.45
  63. spimfv
  64. chvarfv
  65. cbv3v2
  66. sbalex
  67. sbalexOLD
  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. sbcovOLD
  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. equs5av
  101. 2sb5
  102. dfsb7
  103. sbn
  104. sbex
  105. nf5
  106. nf6
  107. nf5d
  108. nf5di
  109. 19.9h
  110. 19.21h
  111. 19.23h
  112. exlimih
  113. exlimdh
  114. equsalhw
  115. equsexhv
  116. hba1
  117. hbnt
  118. hbn
  119. hbnd
  120. hbim1
  121. hbimd
  122. hbim
  123. hban
  124. hb3an
  125. sbi2
  126. sbim
  127. sbrim
  128. sblim
  129. sbor
  130. sbbi
  131. sblbis
  132. sbrbis
  133. sbrbif
  134. sbnf
  135. sbiev
  136. sbievOLD
  137. sbiedw
  138. axc7
  139. axc7e
  140. modal-b
  141. 19.9ht
  142. axc4
  143. axc4i
  144. nfal
  145. nfex
  146. hbex
  147. nfnf
  148. 19.12
  149. nfald
  150. nfexd
  151. nfsbv
  152. sbco2v
  153. aaan
  154. eeor
  155. cbv3v
  156. cbv1v
  157. cbv2w
  158. cbvaldw
  159. cbvexdw
  160. cbv3hv
  161. cbvalv1
  162. cbvexv1
  163. cbval2v
  164. cbvex2v
  165. dvelimhw
  166. pm11.53
  167. 19.12vv
  168. eean
  169. eeanv
  170. eeeanv
  171. ee4anv
  172. ee4anvOLD
  173. sb8v
  174. sb8f
  175. sb8ef
  176. 2sb8ef
  177. sb6rfv
  178. sbnf2
  179. exsb
  180. 2exsb
  181. sbbib
  182. sbbibvv
  183. cbvsbvf
  184. cleljustALT
  185. cleljustALT2
  186. equs5aALT
  187. equs5eALT
  188. axc11r
  189. dral1v
  190. drex1v
  191. drnf1v