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. sbnfOLD
  136. sbiev
  137. sbievOLD
  138. sbiedw
  139. axc7
  140. axc7e
  141. modal-b
  142. 19.9ht
  143. axc4
  144. axc4i
  145. nfal
  146. nfex
  147. hbex
  148. nfnf
  149. 19.12
  150. nfald
  151. nfexd
  152. nfsbv
  153. sbco2v
  154. aaan
  155. eeor
  156. cbv3v
  157. cbv1v
  158. cbv2w
  159. cbvaldw
  160. cbvexdw
  161. cbv3hv
  162. cbvalv1
  163. cbvexv1
  164. cbval2v
  165. cbvex2v
  166. dvelimhw
  167. pm11.53
  168. 19.12vv
  169. eean
  170. eeanv
  171. eeeanv
  172. ee4anv
  173. ee4anvOLD
  174. sb8v
  175. sb8f
  176. sb8ef
  177. 2sb8ef
  178. sb6rfv
  179. sbnf2
  180. exsb
  181. 2exsb
  182. sbbib
  183. sbbibvv
  184. cbvsbvf
  185. cleljustALT
  186. cleljustALT2
  187. equs5aALT
  188. equs5eALT
  189. axc11r
  190. dral1v
  191. drex1v
  192. drnf1v