Theorem eqin1 ≪ | index | src | ≫ 

theorem eqin1 (A B: set): $ A C_ B <-> A i^i B == A $;
StepHypRefExpression
1 inss1 
A i^i B C_ A
2 1 a1i 
A C_ B -> A i^i B C_ A
3 ssin 
A C_ A i^i B <-> A C_ A /\ A C_ B
4 ssid 
A C_ A
5 4 a1i 
A C_ B -> A C_ A
6 id 
A C_ B -> A C_ B
7 5, 6 iand 
A C_ B -> A C_ A /\ A C_ B
8 3, 7 sylibr 
A C_ B -> A C_ A i^i B
9 2, 8 ssasymd 
A C_ B -> A i^i B == A
10 inss2 
A i^i B C_ B
11 sseq1 
A i^i B == A -> (A i^i B C_ B <-> A C_ B)
12 10, 11 mpbii 
A i^i B == A -> A C_ B
13 9, 12 ibii 
A C_ B <-> A i^i B == A

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)