Theorem elall | index | src |

theorem elall (A: set) (l x: nat): $ all A l -> x IN l -> x e. A $;
StepHypRefExpression
1 eleq1
a1 = x -> (a1 e. lmems l <-> x e. lmems l)
2 1 conv lmem
a1 = x -> (a1 e. lmems l <-> x IN l)
3 eleq1
a1 = x -> (a1 e. A <-> x e. A)
4 2, 3 imeqd
a1 = x -> (a1 e. lmems l -> a1 e. A <-> x IN l -> x e. A)
5 4 eale
A. a1 (a1 e. lmems l -> a1 e. A) -> x IN l -> x e. A
6 5 conv all, subset
all A l -> x IN l -> x e. A

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_12), axs_set (ax_8)