Metamath Proof Explorer

Definition df-bnj13

Description: Define the following predicate: R is set-like on A . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion df-bnj13 
|- ( R _Se A <-> A. x e. A _pred ( x , A , R ) e. _V )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR 
 |-  R
1 cA 
 |-  A
2 1 0 w-bnj13 
 |-  R _Se A
3 vx 
 |-  x
4 3 cv 
 |-  x
5 1 0 4 c-bnj14 
 |-  _pred ( x , A , R )
6 cvv 
 |-  _V
7 5 6 wcel 
 |-  _pred ( x , A , R ) e. _V
8 7 3 1 wral 
 |-  A. x e. A _pred ( x , A , R ) e. _V
9 2 8 wb 
 |-  ( R _Se A <-> A. x e. A _pred ( x , A , R ) e. _V )