Step
*
1
1
1
1
of Lemma
bag-member-map
1. T : Type
2. U : Type
3. x : U
4. f : T ⟶ U
5. x ↓∈ {}
⊢ ↓∃v:T. (v ↓∈ {} ∧ (x = (f v) ∈ U))
BY
{ BagMemberD (-1) }
Latex:
Latex:
1.  T  :  Type
2.  U  :  Type
3.  x  :  U
4.  f  :  T  {}\mrightarrow{}  U
5.  x  \mdownarrow{}\mmember{}  \{\}
\mvdash{}  \mdownarrow{}\mexists{}v:T.  (v  \mdownarrow{}\mmember{}  \{\}  \mwedge{}  (x  =  (f  v)))
By
Latex:
BagMemberD  (-1)
Home
Index