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  6106  relmptopab  6223  1st2nd  6343  1stdm  6344  releldm2  6347  reldmtpos  6418  dmtpos  6421  dftpos4  6428  tpostpos  6429  iinerm  6775  fundmen  6980  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  relelbasov  13144  reldvg  15402