Colin Howson,  Logic with trees Chapter 11
Set theory is an extensive topic introduced elsewhere. It can be written as a first order theory.
There is one axiom schema, Abstraction (or Comprehension), which can generate infinitely many axioms
1/10/09 13 Software
Some predicate logic proofs or derivations using Gentzen calculus. Try to prove them (click 'Derive It' off the Wizard Menu, if you want help).