Theorem exeq | index | src |

theorem exeq {x: nat} (a b: wff x): $ A. x (a <-> b) -> (E. x a <-> E. x b) $;
StepHypRefExpression
1 aleq
A. x (~a <-> ~b) -> (A. x ~a <-> A. x ~b)
2 noteq
(a <-> b) -> (~a <-> ~b)
3 2 alimi
A. x (a <-> b) -> A. x (~a <-> ~b)
4 1, 3 syl
A. x (a <-> b) -> (A. x ~a <-> A. x ~b)
5 4 noteqd
A. x (a <-> b) -> (~A. x ~a <-> ~A. x ~b)
6 5 conv ex
A. 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)