Metamath Proof Explorer


Table of Contents - 1.5.4. Axiom scheme ax-13 (Quantified Equality)

  1. ax-13
  2. ax13v
  3. ax13lem1
  4. ax13
  5. ax13lem2
  6. nfeqf2
  7. dveeq2
  8. nfeqf1
  9. dveeq1
  10. nfeqf
  11. axc9
  12. ax6e
  13. ax6
  14. axc10
  15. spimt
  16. spim
  17. spimed
  18. spime
  19. spimv
  20. spimvALT
  21. spimev
  22. spv
  23. spei
  24. chvar
  25. chvarv
  26. cbv3
  27. cbval
  28. cbvex
  29. cbvalv
  30. cbvexv
  31. cbvalvOLD
  32. cbvexvOLD
  33. cbv1
  34. cbv2
  35. cbv3h
  36. cbv1h
  37. cbv2h
  38. cbv2OLD
  39. cbvald
  40. cbvexd
  41. cbvaldva
  42. cbvexdva
  43. cbval2
  44. cbval2OLD
  45. cbvex2
  46. cbval2vv
  47. cbvex2vv
  48. cbvex4v
  49. equs4
  50. equsal
  51. equsex
  52. equsexALT
  53. equsalh
  54. equsexh
  55. axc15
  56. ax12
  57. ax12b
  58. ax13ALT
  59. axc11n
  60. aecom
  61. aecoms
  62. naecoms
  63. axc11
  64. hbae
  65. hbnae
  66. nfae
  67. nfnae
  68. hbnaes
  69. axc16i
  70. axc16nfALT
  71. dral2
  72. dral1
  73. dral1ALT
  74. drex1
  75. drex2
  76. drnf1
  77. drnf2
  78. nfald2
  79. nfexd2
  80. exdistrf
  81. dvelimf
  82. dvelimdf
  83. dvelimh
  84. dvelim
  85. dvelimv
  86. dvelimnf
  87. dveeq2ALT
  88. equvini
  89. equviniOLD
  90. equvel
  91. equs5a
  92. equs5e
  93. equs45f
  94. equs5
  95. dveel1
  96. dveel2
  97. axc14
  98. sb6x
  99. sbequ5
  100. sbequ6
  101. sb5rf
  102. sb6rf
  103. ax12vALT
  104. 2ax6elem
  105. 2ax6e
  106. 2ax6eOLD
  107. 2sb5rf
  108. 2sb6rf
  109. sbel2x
  110. sb4b
  111. sb4bOLD
  112. sb3b
  113. sb3
  114. sb1
  115. sb2
  116. sb3OLD
  117. sb4OLD
  118. sb1OLD
  119. sb3bOLD
  120. sb4a
  121. dfsb1
  122. spsbeOLDOLD
  123. sb2vOLDOLD
  124. sb4vOLDOLD
  125. sbequ2OLDOLD
  126. sbimiOLD
  127. sbimdvOLD
  128. equsb1vOLDOLD
  129. sbimdOLD
  130. sbtvOLD
  131. sbequ1OLD
  132. hbsb2
  133. nfsb2
  134. hbsb2a
  135. sb4e
  136. hbsb2e
  137. hbsb3
  138. nfs1
  139. axc16ALT
  140. axc16gALT
  141. equsb1
  142. equsb2
  143. dfsb2
  144. dfsb3
  145. sbequiOLD
  146. drsb1
  147. sb2ae
  148. sb6f
  149. sb5f
  150. nfsb4t
  151. nfsb4
  152. sbnOLD
  153. sbi1OLD
  154. sbequ8
  155. sbie
  156. sbied
  157. sbiedv
  158. 2sbiev
  159. sbcom3
  160. sbco
  161. sbid2
  162. sbid2v
  163. sbidm
  164. sbco2
  165. sbco2d
  166. sbco3
  167. sbcom
  168. sbtrt
  169. sbtr
  170. sb8
  171. sb8e
  172. sb9
  173. sb9i
  174. sbhb
  175. nfsbd
  176. nfsb
  177. nfsbOLD
  178. hbsb
  179. sb7f
  180. sb7h
  181. dfsb7OLDOLD
  182. sb10f
  183. sbal1
  184. sbal2
  185. sbal2OLD
  186. sbalOLD
  187. 2sb8e