Definition df-rel 4758

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

This definition is referenced by:  brrelex12  4790  0nelrel  4798  releq  4834  nfrel  4837  sbcrel  4838  relss  4839  ssrel  4840  elrel  4854  relsng  4855  relsn  4857  relxp  4861  relun  4871  reliun  4875  reliin  4876  rel0  4879  relopabiv  4880  relopabi  4882  relop  4907  eqbrrdva  4927  elreldm  4985  issref  5147  cnvcnv  5217  relrelss  5291  cnviinm  5306  nfunv  5387  funinsn  5407  oprabss  6141  relmptopab  6258  1st2nd  6377  1stdm  6378  releldm2  6381  reldmtpos  6486  dmtpos  6489  dftpos4  6496  tpostpos  6497  iinerm  6843  fundmen  7049  frecuzrdgtcl  10778  frecuzrdgfunlem  10785  relelbasov  13292  reldvg  15561