Definition df-rel 5632

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 6148 and dfrel3 6157. (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 5630	. 2 wff Rel 𝐴
3		cvv 3441	. . . 4 class V
4	3, 3	cxp 5623	. . 3 class (V × V)
5	1, 4	wss 3902	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 206	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  relxp  5643  pwvrel  5675  brrelex12  5677  0nelrel0  5685  releq  5727  nfrel  5730  sbcrel  5731  relss  5732  ssrel  5733  elrel  5748  rel0  5749  nrelv  5750  relsng  5751  relun  5761  reliun  5766  reliin  5767  relopabiv  5770  relopabi  5772  relopabiALT  5773  exopxfr2  5794  relop  5800  eqbrrdva  5819  elreldm  5885  cnvcnv  6151  relrelss  6232  cnviin  6245  dff3  7047  oprabss  7468  relmptopab  7610  1st2nd  7985  1stdm  7986  releldm2  7989  relmpoopab  8038  reldmtpos  8178  dmtpos  8182  dftpos4  8189  tpostpos  8190  iiner  8730  fundmen  8972  nqerf  10845  uzrdgfni  13885  hashfun  14364  reltrclfv  14944  homarel  17964  relxpchom  18108  nfchnd  18538  ustrel  24160  utop2nei  24198  utop3cls  24199  metustrel  24500  pi1xfrcnv  25017  reldv  25831  dvbsss  25863  ssrelf  32696  1stpreimas  32787  fpwrelmap  32814  gsumhashmul  33152  metideq  34052  metider  34053  pstmfval  34055  esum2d  34252  txprel  36073  relsset  36082  elfuns  36109  fnsingle  36113  funimage  36122  bj-opelrelex  37351  bj-elid5  37376  mblfinlem1  37860  rngosn3  38127  xrnrel  38585  elrelsrel  38645  dihvalrel  41607  cnvcnvintabd  43908  cnvintabd  43911  clcnvlem  43931  rfovcnvf1od  44312  relopabVD  45208  sprsymrelfo  47810  dmtposss  49188  oppff1  49460  fuco2eld2  49626  fuco22a  49662