Metamath Proof Explorer

Definition df-se

Description: Define the set-like predicate. (Contributed by Mario Carneiro, 19-Nov-2014)

Ref Expression
Assertion df-se 
|- ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 
 |-  R
1 cA 
 |-  A
2 1 0 wse 
 |-  R Se A
3 vx 
 |-  x
4 vy 
 |-  y
5 4 cv 
 |-  y
6 3 cv 
 |-  x
7 5 6 0 wbr 
 |-  y R x
8 7 4 1 crab 
 |-  { y e. A | y R x }
9 cvv 
 |-  _V
10 8 9 wcel 
 |-  { y e. A | y R x } e. _V
11 10 3 1 wral 
 |-  A. x e. A { y e. A | y R x } e. _V
12 2 11 wb 
 |-  ( R Se A <-> A. x e. A { y e. A | y R x } e. _V )