Definition df-rel 4726

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

This definition is referenced by:  brrelex12  4757  0nelrel  4765  releq  4801  nfrel  4804  sbcrel  4805  relss  4806  ssrel  4807  elrel  4821  relsng  4822  relsn  4824  relxp  4828  relun  4836  reliun  4840  reliin  4841  rel0  4844  relopabiv  4845  relopabi  4847  relop  4872  eqbrrdva  4892  elreldm  4950  issref  5111  cnvcnv  5181  relrelss  5255  cnviinm  5270  nfunv  5351  funinsn  5370  oprabss  6096  relmptopab  6213  1st2nd  6333  1stdm  6334  releldm2  6337  reldmtpos  6405  dmtpos  6408  dftpos4  6415  tpostpos  6416  iinerm  6762  fundmen  6967  frecuzrdgtcl  10642  frecuzrdgfunlem  10649  relelbasov  13103  reldvg  15361