Definition df-rel 4732

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

This definition is referenced by:  brrelex12  4764  0nelrel  4772  releq  4808  nfrel  4811  sbcrel  4812  relss  4813  ssrel  4814  elrel  4828  relsng  4829  relsn  4831  relxp  4835  relun  4844  reliun  4848  reliin  4849  rel0  4852  relopabiv  4853  relopabi  4855  relop  4880  eqbrrdva  4900  elreldm  4958  issref  5119  cnvcnv  5189  relrelss  5263  cnviinm  5278  nfunv  5359  funinsn  5379  oprabss  6107  relmptopab  6224  1st2nd  6344  1stdm  6345  releldm2  6348  reldmtpos  6419  dmtpos  6422  dftpos4  6429  tpostpos  6430  iinerm  6776  fundmen  6981  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  relelbasov  13163  reldvg  15422