Theorem exor | index | src |

theorem exor {x: nat} (a b: wff x): $ E. x (a \/ b) <-> E. x a \/ E. x b $;
StepHypRefExpression
1 bitr
(E. x (a \/ b) <-> ~(A. x ~a /\ A. x ~b)) -> (~(A. x ~a /\ A. x ~b) <-> E. x a \/ E. x b) -> (E. x (a \/ b) <-> E. x a \/ E. x b)
2 bitr
(A. x ~(a \/ b) <-> A. x (~a /\ ~b)) -> (A. x (~a /\ ~b) <-> A. x ~a /\ A. x ~b) -> (A. x ~(a \/ b) <-> A. x ~a /\ A. x ~b)
3 notor
~(a \/ b) <-> ~a /\ ~b
4 3 aleqi
A. x ~(a \/ b) <-> A. x (~a /\ ~b)
5 2, 4 ax_mp
(A. x (~a /\ ~b) <-> A. x ~a /\ A. x ~b) -> (A. x ~(a \/ b) <-> A. x ~a /\ A. x ~b)
6 alan
A. x (~a /\ ~b) <-> A. x ~a /\ A. x ~b
7 5, 6 ax_mp
A. x ~(a \/ b) <-> A. x ~a /\ A. x ~b
8 7 noteqi
~A. x ~(a \/ b) <-> ~(A. x ~a /\ A. x ~b)
9 8 conv ex
E. x (a \/ b) <-> ~(A. x ~a /\ A. x ~b)
10 1, 9 ax_mp
(~(A. x ~a /\ A. x ~b) <-> E. x a \/ E. x b) -> (E. x (a \/ b) <-> E. x a \/ E. x b)
11 notan
~(A. x ~a /\ A. x ~b) <-> ~A. x ~a \/ ~A. x ~b
12 11 conv ex
~(A. x ~a /\ A. x ~b) <-> E. x a \/ E. x b
13 10, 12 ax_mp
E. x (a \/ b) <-> E. x a \/ E. x b

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4)