Definition df-rel 4667

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

This definition is referenced by:  brrelex12  4698  0nelrel  4706  releq  4742  nfrel  4745  sbcrel  4746  relss  4747  ssrel  4748  elrel  4762  relsng  4763  relsn  4765  relxp  4769  relun  4777  reliun  4781  reliin  4782  rel0  4785  relopabiv  4786  relopabi  4788  relop  4813  eqbrrdva  4833  elreldm  4889  issref  5049  cnvcnv  5119  relrelss  5193  cnviinm  5208  nfunv  5288  funinsn  5304  oprabss  6005  1st2nd  6236  1stdm  6237  releldm2  6240  reldmtpos  6308  dmtpos  6311  dftpos4  6318  tpostpos  6319  iinerm  6663  fundmen  6862  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  relelbasov  12683  reldvdsrsrg  13591  reldvg  14858