Definition df-rel 5641

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

This definition is referenced by:  relxp  5652  pwvrel  5684  brrelex12  5686  0nelrel0  5694  releq  5736  nfrel  5739  sbcrel  5740  relss  5741  ssrel  5742  elrel  5757  rel0  5758  nrelv  5759  relsng  5760  relun  5770  reliun  5775  reliin  5776  relopabiv  5779  relopabi  5781  relopabiALT  5782  exopxfr2  5803  relop  5809  eqbrrdva  5828  elreldm  5894  cnvcnv  6160  relrelss  6241  cnviin  6254  dff3  7056  oprabss  7478  relmptopab  7620  1st2nd  7995  1stdm  7996  releldm2  7999  relmpoopab  8048  reldmtpos  8188  dmtpos  8192  dftpos4  8199  tpostpos  8200  iiner  8740  fundmen  8982  nqerf  10855  uzrdgfni  13895  hashfun  14374  reltrclfv  14954  homarel  17974  relxpchom  18118  nfchnd  18548  ustrel  24173  utop2nei  24211  utop3cls  24212  metustrel  24513  pi1xfrcnv  25030  reldv  25844  dvbsss  25876  ssrelf  32711  1stpreimas  32802  fpwrelmap  32829  gsumhashmul  33167  metideq  34077  metider  34078  pstmfval  34080  esum2d  34277  txprel  36099  relsset  36108  elfuns  36135  fnsingle  36139  funimage  36148  bj-opelrelex  37426  bj-elid5  37451  mblfinlem1  37937  rngosn3  38204  xrnrel  38662  elrelsrel  38722  dihvalrel  41684  cnvcnvintabd  43985  cnvintabd  43988  clcnvlem  44008  rfovcnvf1od  44389  relopabVD  45285  sprsymrelfo  47886  dmtposss  49264  oppff1  49536  fuco2eld2  49702  fuco22a  49738