Theorem all2ss | index | src |

theorem all2ss (R S: set): $ R C_ S -> all2 R C_ all2 S $;
StepHypRefExpression
1 all2ssg
A. a3 A. a4 (a3 IN a1 /\ a4 IN a2 -> a3, a4 e. R -> a3, a4 e. S) -> a1, a2 e. all2 R -> a1, a2 e. all2 S
2 ssel
R C_ S -> a3, a4 e. R -> a3, a4 e. S
3 2 a1d
R C_ S -> a3 IN a1 /\ a4 IN a2 -> a3, a4 e. R -> a3, a4 e. S
4 3 iald
R C_ S -> A. a4 (a3 IN a1 /\ a4 IN a2 -> a3, a4 e. R -> a3, a4 e. S)
5 4 iald
R C_ S -> A. a3 A. a4 (a3 IN a1 /\ a4 IN a2 -> a3, a4 e. R -> a3, a4 e. S)
6 1, 5 syl
R C_ S -> a1, a2 e. all2 R -> a1, a2 e. all2 S
7 6 ssrd2
R C_ S -> all2 R C_ all2 S

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)