Definition df-rel 4546

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4989 and dfrel3 4996. (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 4544	. 2 wff Rel 𝐴
3		cvv 2686	. . . 4 class V
4	3, 3	cxp 4537	. . 3 class (V × V)
5	1, 4	wss 3071	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 104	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  brrelex12  4577  0nelrel  4585  releq  4621  nfrel  4624  sbcrel  4625  relss  4626  ssrel  4627  elrel  4641  relsng  4642  relsn  4644  relxp  4648  relun  4656  reliun  4660  reliin  4661  rel0  4664  relopabi  4665  relop  4689  eqbrrdva  4709  elreldm  4765  issref  4921  cnvcnv  4991  relrelss  5065  cnviinm  5080  nfunv  5156  funinsn  5172  oprabss  5857  1st2nd  6079  1stdm  6080  releldm2  6083  reldmtpos  6150  dmtpos  6153  dftpos4  6160  tpostpos  6161  iinerm  6501  fundmen  6700  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  reldvg  12817