Theorem Ifpos ≪ | index | src | ≫

theorem Ifpos (A B: set) (p: wff): $ p -> If p A B == A $;

p -> (ifp p (n e. A) (n e. B) <-> n e. A)

p -> {n | ifp p (n e. A) (n e. B)} == A

p -> If p A B == A

Axiom use