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. cbv1
  32. cbv2
  33. cbv3h
  34. cbv1h
  35. cbv2h
  36. cbvald
  37. cbvexd
  38. cbvaldva
  39. cbvexdva
  40. cbval2
  41. cbvex2
  42. cbval2vv
  43. cbvex2vv
  44. cbvex4v
  45. equs4
  46. equsal
  47. equsex
  48. equsexALT
  49. equsalh
  50. equsexh
  51. axc15
  52. ax12
  53. ax12b
  54. ax13ALT
  55. axc11n
  56. aecom
  57. aecoms
  58. naecoms
  59. axc11
  60. hbae
  61. hbnae
  62. nfae
  63. nfnae
  64. hbnaes
  65. axc16i
  66. axc16nfALT
  67. dral2
  68. dral1
  69. dral1ALT
  70. drex1
  71. drex2
  72. drnf1
  73. drnf2
  74. nfald2
  75. nfexd2
  76. exdistrf
  77. dvelimf
  78. dvelimdf
  79. dvelimh
  80. dvelim
  81. dvelimv
  82. dvelimnf
  83. dveeq2ALT
  84. equvini
  85. equvel
  86. equs5a
  87. equs5e
  88. equs45f
  89. equs5
  90. dveel1
  91. dveel2
  92. axc14
  93. sb6x
  94. sbequ5
  95. sbequ6
  96. sb5rf
  97. sb6rf
  98. ax12vALT
  99. 2ax6elem
  100. 2ax6e
  101. 2sb5rf
  102. 2sb6rf
  103. sbel2x
  104. sb4b
  105. sb3b
  106. sb3
  107. sb1
  108. sb2
  109. sb4a
  110. dfsb1
  111. hbsb2
  112. nfsb2
  113. hbsb2a
  114. sb4e
  115. hbsb2e
  116. hbsb3
  117. nfs1
  118. axc16ALT
  119. axc16gALT
  120. equsb1
  121. equsb2
  122. dfsb2
  123. dfsb3
  124. drsb1
  125. sb2ae
  126. sb6f
  127. sb5f
  128. nfsb4t
  129. nfsb4
  130. sbequ8
  131. sbie
  132. sbied
  133. sbiedv
  134. 2sbiev
  135. sbcom3
  136. sbco
  137. sbid2
  138. sbid2v
  139. sbidm
  140. sbco2
  141. sbco2d
  142. sbco3
  143. sbcom
  144. sbtrt
  145. sbtr
  146. sb8
  147. sb8e
  148. sb9
  149. sb9i
  150. sbhb
  151. nfsbd
  152. nfsb
  153. hbsb
  154. sb7f
  155. sb7h
  156. sb10f
  157. sbal1
  158. sbal2
  159. 2sb8e