Definition df-rel 4378

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4801 and dfrel3 4808. (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 4376	. 2 wff Rel 𝐴
3		cvv 2602	. . . 4 class V
4	3, 3	cxp 4369	. . 3 class (V × V)
5	1, 4	wss 2974	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 103	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  brrelex12  4407  releq  4448  nfrel  4451  sbcrel  4452  relss  4453  ssrel  4454  elrel  4468  relsng  4469  relsn  4471  relxp  4475  relun  4482  reliun  4486  reliin  4487  rel0  4490  relopabi  4491  relop  4514  eqbrrdva  4533  elreldm  4588  issref  4737  cnvcnv  4803  relrelss  4874  cnviinm  4889  nfunv  4963  funinsn  4979  oprabss  5621  1st2nd  5838  1stdm  5839  releldm2  5842  reldmtpos  5902  dmtpos  5905  dftpos4  5912  tpostpos  5913  iinerm  6244  fundmen  6353  frecuzrdgtcl  9494  frecuzrdgfunlem  9501