Metamath Proof Explorer

Table of Contents - 1.5.2. Axiom scheme ax-11 (Quantifier Commutation)

  1. ax-11
  2. alcoms
  3. alcom
  4. alrot3
  5. alrot4
  6. excom
  7. excomim
  8. excom13
  9. exrot3
  10. exrot4
  11. hbal
  12. hbald
  13. sbal
  14. sbalv
  15. hbsbw
  16. hbsbwOLD
  17. sbcom2
  18. sbco4lemOLD
  19. sbco4OLD
  20. nfa2