Theorem unss ≪ | index | src | ≫ 

theorem unss (A B C: set): $ A u. B C_ C <-> A C_ C /\ B C_ C $;
StepHypRefExpression
1 sstr 
A C_ A u. B -> A u. B C_ C -> A C_ C
2 ssun1 
A C_ A u. B
3 1, 2 ax_mp 
A u. B C_ C -> A C_ C
4 sstr 
B C_ A u. B -> A u. B C_ C -> B C_ C
5 ssun2 
B C_ A u. B
6 4, 5 ax_mp 
A u. B C_ C -> B C_ C
7 3, 6 iand 
A u. B C_ C -> A C_ C /\ B C_ C
8 elun 
x e. A u. B <-> x e. A \/ x e. B
9 ssel 
A C_ C -> x e. A -> x e. C
10 9 anwl 
A C_ C /\ B C_ C -> x e. A -> x e. C
11 ssel 
B C_ C -> x e. B -> x e. C
12 11 anwr 
A C_ C /\ B C_ C -> x e. B -> x e. C
13 10, 12 eord 
A C_ C /\ B C_ C -> x e. A \/ x e. B -> x e. C
14 8, 13 syl5bi 
A C_ C /\ B C_ C -> x e. A u. B -> x e. C
15 14 iald 
A C_ C /\ B C_ C -> A. x (x e. A u. B -> x e. C)
16 15 conv subset 
A C_ C /\ B C_ C -> A u. B C_ C
17 7, 16 ibii 
A u. B C_ C <-> A C_ C /\ B C_ C

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)