Definition df-rel 4703

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5155 and dfrel3 5162. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-rel	⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

Detailed syntax breakdown of Definition df-rel

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wrel 4701	. 2 wff Rel 𝐴
3		cvv 2779	. . . 4 class V
4	3, 3	cxp 4694	. . 3 class (V × V)
5	1, 4	wss 3177	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 105	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  brrelex12  4734  0nelrel  4742  releq  4778  nfrel  4781  sbcrel  4782  relss  4783  ssrel  4784  elrel  4798  relsng  4799  relsn  4801  relxp  4805  relun  4813  reliun  4817  reliin  4818  rel0  4821  relopabiv  4822  relopabi  4824  relop  4849  eqbrrdva  4869  elreldm  4926  issref  5087  cnvcnv  5157  relrelss  5231  cnviinm  5246  nfunv  5327  funinsn  5346  oprabss  6061  1st2nd  6297  1stdm  6298  releldm2  6301  reldmtpos  6369  dmtpos  6372  dftpos4  6379  tpostpos  6380  iinerm  6724  fundmen  6929  frecuzrdgtcl  10601  frecuzrdgfunlem  10608  relelbasov  13061  reldvdsrsrg  14021  reldvg  15318