Definition df-rel 5656

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 6177 and dfrel3 6187. (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 5654	. 2 wff Rel 𝐴
3		cvv 3456	. . . 4 class V
4	3, 3	cxp 5647	. . 3 class (V × V)
5	1, 4	wss 3906	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 208	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  relxp  5667  pwvrel  5699  brrelex12  5701  0nelrel0  5709  releq  5751  nfrel  5754  sbcrel  5755  relss  5756  ssrel  5757  elrel  5772  rel0  5773  nrelvOLD  5775  relsng  5776  relun  5786  reliun  5791  reliin  5792  relopabiv  5795  relopabi  5797  relopabiALT  5798  exopxfr2  5818  relop  5824  eqbrrdva  5843  elreldm  5913  cnvcnv  6180  relrelss  6262  cnviin  6275  dff3  7083  oprabss  7506  relmptopab  7648  1st2nd  8022  1stdm  8023  releldm2  8026  relmpoopab  8075  reldmtpos  8216  dmtpos  8220  dftpos4  8227  tpostpos  8228  iiner  8773  fundmen  9014  nqerf  10890  uzrdgfni  13973  hashfun  14452  reltrclfv  15032  homarel  18071  relxpchom  18215  nfchnd  18645  ustrel  24274  utop2nei  24312  utop3cls  24313  metustrel  24614  pi1xfrcnv  25121  reldv  25934  dvbsss  25966  ssrelf  32819  1stpreimas  32910  fpwrelmap  32937  gsumhashmul  33249  metideq  34192  metider  34193  pstmfval  34195  esum2d  34392  txprel  36232  relsset  36241  elfuns  36268  fnsingle  36272  funimage  36281  bj-opelrelex  37641  bj-elid5  37666  mblfinlem1  38161  rngosn3  38428  xrnrel  38886  elrelsrel  38946  dihvalrel  41908  cnvcnvintabd  44181  cnvintabd  44184  clcnvlem  44204  rfovcnvf1od  44585  relopabVD  45481  sprsymrelfo  48108  dmtposss  49502  oppff1  49774  fuco2eld2  49940  fuco22a  49976