Set membership and type judgements

Stream: new members

[Aniruddh Agarwal]

Potentially dumb question. Are ex1 and ex2 below equivalent:

universe u

variable {α : Type u}

def P (a : α) (b : α) : Prop := sorry

def ex1 (S : set α) := { x : α | ∀ y : α, y ∈ S → P x y }
def ex2 (S : set α) := { x : α | ∀ y ∈ S, P x y }

[Kenny Lau]

yes, definitionally

[Kevin Buzzard]

You can check to see if rfl proves that they are equal

[Aniruddh Agarwal]

Good idea!