x:T. x 
c1 
x c2T:Type, c1,c2:Collection(T). c1 = c2 Prop c == c(x)T:Type, x:T, c:Collection(T). x c Prop Q == (P 
Q) & (P Q)A,B:Prop. (A B) Prop Q == Q PA,B:Prop. (A B) Prop| Who Cites col equal? | |
| col_equal | Def c1 = c2 == x:T. x c1 x c2 |
| Thm* T:Type, c1,c2:Collection(T). c1 = c2 Prop | |
| col_member |
Def x c == c(x) |
| Thm* T:Type, x:T, c:Collection(T). x c Prop | |
| iff |
Def P Q == (P Q) & (P Q) |
| Thm* A,B:Prop. (A B) Prop | |
| rev_implies |
Def P Q == Q P |
| Thm* A,B:Prop. (A B) Prop |
| Syntax: | c1 = c2 | has structure: | col_equal(T; c1; c2) |
About:
 |  |  |  |  |  |  |  |