A relation class is a formula with two free variables.

Well-Founded Local Extensional