Definition df-rel 4779

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

This definition is referenced by:  brrelex12  4811  0nelrel  4819  releq  4855  nfrel  4858  sbcrel  4859  relss  4860  ssrel  4861  elrel  4875  relsng  4876  relsn  4878  relxp  4882  relun  4892  reliun  4896  reliin  4897  rel0  4900  relopabiv  4901  relopabi  4903  relop  4928  eqbrrdva  4948  elreldm  5006  issref  5168  cnvcnv  5238  relrelss  5312  cnviinm  5327  nfunv  5408  funinsn  5428  oprabss  6167  relmptopab  6284  1st2nd  6408  1stdm  6409  releldm2  6412  reldmtpos  6517  dmtpos  6520  dftpos4  6527  tpostpos  6528  iinerm  6874  fundmen  7087  frecuzrdgtcl  10830  frecuzrdgfunlem  10837  relelbasov  13396  reldvg  15706