This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-rel

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 ⊆ V × V

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 0 wrel wff Rel ⁡ A
2 cvv class V
3 2 2 cxp class V × V
4 0 3 wss wff A ⊆ V × V
5 1 4 wb wff Rel ⁡ A ↔ A ⊆ V × V