Theorems · Theorem · logic and foundations
ZFSet.mem_image
∀ {f : ZFSet.{u} → ZFSet.{u}} [inst : ZFSet.Definable₁ f] {x y : ZFSet.{u}}, y ∈ ZFSet.image f x ↔ ∃ z ∈ x, f z = y- Defined in
- Mathlib.SetTheory.ZFC.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 37 from the axioms · uses propext, Quot.sound
- Assumes
- ZFSet.Definable₁
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ZFSetstatement and proof · cited by 259
- PSetproof · cited by 107
- PSet.Equivproof · cited by 44
- PSet.Typeproof · cited by 34
- PSet.Funcproof · cited by 29
- ZFSet.Definable₁statement and proof · cited by 10
- PSet.Mem.mkproof · cited by 9
- ZFSet.imagestatement and proof · cited by 4
- ZFSet.Definable₁.outproof · cited by 3
- ZFSet.image.mkproof · cited by 3
- ZFSet.Definable₁.mk_outproof · cited by 2
- PSet.imageproof · cited by 2
Cited by3
Results whose statement or proof uses this declaration.
- ZFSet.map_isFuncproof · cited by 1
- ZFSet.map_uniqueproof · cited by 1
- ZFSet.mem_mapproof · cited by 1