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. 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. sb4av
  68. sbimd
  69. sbbid
  70. 2sbbid
  71. sbequ1
  72. sbequ2
  73. sbequ2OLD
  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. sb5OLD
  100. sb56OLD
  101. equs5av
  102. 2sb5
  103. sbco4lem
  104. sbco4lemOLD
  105. sbco4
  106. dfsb7
  107. sbn
  108. sbex
  109. nf5
  110. nf6
  111. nf5d
  112. nf5di
  113. 19.9h
  114. 19.21h
  115. 19.23h
  116. exlimih
  117. exlimdh
  118. equsalhw
  119. equsexhv
  120. hba1
  121. hbnt
  122. hbn
  123. hbnd
  124. hbim1
  125. hbimd
  126. hbim
  127. hban
  128. hb3an
  129. sbi2
  130. sbim
  131. sbrim
  132. sbrimv
  133. sblim
  134. sbor
  135. sbbi
  136. sblbis
  137. sbrbis
  138. sbrbif
  139. sbiev
  140. sbiedw
  141. sbiedwOLD
  142. axc7
  143. axc7e
  144. modal-b
  145. 19.9ht
  146. axc4
  147. axc4i
  148. nfal
  149. nfex
  150. hbex
  151. nfnf
  152. 19.12
  153. nfald
  154. nfexd
  155. nfsbv
  156. hbsbwOLD
  157. sbco2v
  158. aaan
  159. eeor
  160. cbv3v
  161. cbv1v
  162. cbv2w
  163. cbvaldw
  164. cbvexdw
  165. cbv3hv
  166. cbvalv1
  167. cbvexv1
  168. cbval2v
  169. cbval2vOLD
  170. cbvex2v
  171. dvelimhw
  172. pm11.53
  173. 19.12vv
  174. eean
  175. eeanv
  176. eeeanv
  177. ee4anv
  178. sb8v
  179. sb8ev
  180. 2sb8ev
  181. sb6rfv
  182. sbnf2
  183. exsb
  184. 2exsb
  185. sbbib
  186. sbbibvv
  187. cleljustALT
  188. cleljustALT2
  189. equs5aALT
  190. equs5eALT
  191. axc11r
  192. dral1v
  193. drex1v
  194. drnf1v