Definition df-rel 5627

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

This definition is referenced by:  relxp  5638  pwvrel  5670  brrelex12  5672  0nelrel0  5680  releq  5722  nfrel  5725  sbcrel  5726  relss  5727  ssrel  5728  elrel  5743  rel0  5744  nrelv  5745  relsng  5746  relun  5756  reliun  5761  reliin  5762  relopabiv  5765  relopabi  5767  relopabiALT  5768  exopxfr2  5788  relop  5794  eqbrrdva  5813  elreldm  5879  cnvcnv  6145  relrelss  6226  cnviin  6239  dff3  7041  oprabss  7464  relmptopab  7606  1st2nd  7981  1stdm  7982  releldm2  7985  relmpoopab  8033  reldmtpos  8173  dmtpos  8177  dftpos4  8184  tpostpos  8185  iiner  8725  fundmen  8967  nqerf  10842  uzrdgfni  13909  hashfun  14388  reltrclfv  14968  homarel  17992  relxpchom  18136  nfchnd  18566  ustrel  24165  utop2nei  24203  utop3cls  24204  metustrel  24505  pi1xfrcnv  25012  reldv  25825  dvbsss  25857  ssrelf  32676  1stpreimas  32767  fpwrelmap  32794  gsumhashmul  33116  metideq  34025  metider  34026  pstmfval  34028  esum2d  34225  txprel  36047  relsset  36056  elfuns  36083  fnsingle  36087  funimage  36096  bj-opelrelex  37446  bj-elid5  37471  mblfinlem1  37966  rngosn3  38233  xrnrel  38691  elrelsrel  38751  dihvalrel  41713  cnvcnvintabd  44015  cnvintabd  44018  clcnvlem  44038  rfovcnvf1od  44419  relopabVD  45315  sprsymrelfo  47945  dmtposss  49339  oppff1  49611  fuco2eld2  49777  fuco22a  49813