Definition df-rel 4670

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

This definition is referenced by:  brrelex12  4701  0nelrel  4709  releq  4745  nfrel  4748  sbcrel  4749  relss  4750  ssrel  4751  elrel  4765  relsng  4766  relsn  4768  relxp  4772  relun  4780  reliun  4784  reliin  4785  rel0  4788  relopabiv  4789  relopabi  4791  relop  4816  eqbrrdva  4836  elreldm  4892  issref  5052  cnvcnv  5122  relrelss  5196  cnviinm  5211  nfunv  5291  funinsn  5307  oprabss  6008  1st2nd  6239  1stdm  6240  releldm2  6243  reldmtpos  6311  dmtpos  6314  dftpos4  6321  tpostpos  6322  iinerm  6666  fundmen  6865  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  relelbasov  12740  reldvdsrsrg  13648  reldvg  14915