Definition df-rel 4761

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

This definition is referenced by:  brrelex12  4793  0nelrel  4801  releq  4837  nfrel  4840  sbcrel  4841  relss  4842  ssrel  4843  elrel  4857  relsng  4858  relsn  4860  relxp  4864  relun  4874  reliun  4878  reliin  4879  rel0  4882  relopabiv  4883  relopabi  4885  relop  4910  eqbrrdva  4930  elreldm  4988  issref  5150  cnvcnv  5220  relrelss  5294  cnviinm  5309  nfunv  5390  funinsn  5410  oprabss  6147  relmptopab  6264  1st2nd  6388  1stdm  6389  releldm2  6392  reldmtpos  6497  dmtpos  6500  dftpos4  6507  tpostpos  6508  iinerm  6854  fundmen  7060  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  relelbasov  13359  reldvg  15670