Definition df-rel 5684

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 6189 and dfrel3 6198. (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 5682	. 2 wff Rel 𝐴
3		cvv 3475	. . . 4 class V
4	3, 3	cxp 5675	. . 3 class (V × V)
5	1, 4	wss 3949	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 205	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  relxp  5695  pwvrel  5727  brrelex12  5729  0nelrel0  5737  releq  5777  nfrel  5780  sbcrel  5781  relss  5782  ssrel  5783  ssrelOLD  5784  elrel  5799  rel0  5800  nrelv  5801  relsng  5802  relun  5812  reliun  5817  reliin  5818  relopabiv  5821  relopabi  5823  relopabiALT  5824  exopxfr2  5845  relop  5851  eqbrrdva  5870  elreldm  5935  cnvcnv  6192  relrelss  6273  cnviin  6286  dff3  7102  oprabss  7515  relmptopab  7656  1st2nd  8025  1stdm  8026  releldm2  8029  relmpoopab  8080  reldmtpos  8219  dmtpos  8223  dftpos4  8230  tpostpos  8231  iiner  8783  fundmen  9031  nqerf  10925  uzrdgfni  13923  hashfun  14397  reltrclfv  14964  homarel  17986  relxpchom  18133  ustrel  23716  utop2nei  23755  utop3cls  23756  metustrel  24061  pi1xfrcnv  24573  reldv  25387  dvbsss  25419  ssrelf  31875  1stpreimas  31958  fpwrelmap  31989  gsumhashmul  32239  metideq  32904  metider  32905  pstmfval  32907  esum2d  33122  txprel  34882  relsset  34891  elfuns  34918  fnsingle  34922  funimage  34931  bj-opelrelex  36073  bj-elid5  36098  mblfinlem1  36573  rngosn3  36840  xrnrel  37291  elrelsrel  37405  dihvalrel  40198  cnvcnvintabd  42399  cnvintabd  42402  clcnvlem  42422  rfovcnvf1od  42803  relopabVD  43710  sprsymrelfo  46213