Definition df-rel 4781

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5238 and dfrel3 5245. (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 4779	. 2 wff Rel 𝐴
3		cvv 2821	. . . 4 class V
4	3, 3	cxp 4772	. . 3 class (V × V)
5	1, 4	wss 3220	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 105	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is used by:  brrelex12  4813  0nelrel  4821  releq  4857  nfrel  4860  sbcrel  4861  relss  4862  ssrel  4863  elrel  4877  relsng  4878  relsn  4880  relxp  4884  relun  4894  reliun  4898  reliin  4899  rel0  4902  relopabiv  4903  relopabi  4905  relop  4930  eqbrrdva  4950  elreldm  5008  issref  5170  cnvcnv  5240  relrelss  5314  cnviinm  5329  nfunv  5410  funinsn  5430  oprabss  6174  relmptopab  6291  1st2nd  6415  1stdm  6416  releldm2  6419  reldmtpos  6524  dmtpos  6527  dftpos4  6534  tpostpos  6535  iinerm  6881  fundmen  7094  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  relelbasov  13416  reldvg  15780