Definition df-rel 4651

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

This definition is referenced by:  brrelex12  4682  0nelrel  4690  releq  4726  nfrel  4729  sbcrel  4730  relss  4731  ssrel  4732  elrel  4746  relsng  4747  relsn  4749  relxp  4753  relun  4761  reliun  4765  reliin  4766  rel0  4769  relopabi  4770  relop  4795  eqbrrdva  4815  elreldm  4871  issref  5029  cnvcnv  5099  relrelss  5173  cnviinm  5188  nfunv  5268  funinsn  5284  oprabss  5981  1st2nd  6205  1stdm  6206  releldm2  6209  reldmtpos  6277  dmtpos  6280  dftpos4  6287  tpostpos  6288  iinerm  6632  fundmen  6831  frecuzrdgtcl  10442  frecuzrdgfunlem  10449  reldvdsrsrg  13439  reldvg  14600