Description: Define the relation predicate. Definition 6.4(1) of TakeutiZaring p. 23. For alternate definitions, see dfrel2 and dfrel3 . (Contributed by NM, 1-Aug-1994)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-rel | |- ( Rel A <-> A C_ ( _V X. _V ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | |- A |
|
| 1 | 0 | wrel | |- Rel A |
| 2 | cvv | |- _V |
|
| 3 | 2 2 | cxp | |- ( _V X. _V ) |
| 4 | 0 3 | wss | |- A C_ ( _V X. _V ) |
| 5 | 1 4 | wb | |- ( Rel A <-> A C_ ( _V X. _V ) ) |