Definition df-rel 5626

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

This definition is referenced by:  relxp  5637  pwvrel  5669  brrelex12  5671  0nelrel0  5679  releq  5721  nfrel  5724  sbcrel  5725  relss  5726  ssrel  5727  elrel  5742  rel0  5743  nrelv  5744  relsng  5745  relun  5755  reliun  5760  reliin  5761  relopabiv  5764  relopabi  5766  relopabiALT  5767  exopxfr2  5788  relop  5794  eqbrrdva  5813  elreldm  5879  cnvcnv  6144  relrelss  6225  cnviin  6238  dff3  7039  oprabss  7460  relmptopab  7602  1st2nd  7977  1stdm  7978  releldm2  7981  relmpoopab  8030  reldmtpos  8170  dmtpos  8174  dftpos4  8181  tpostpos  8182  iiner  8719  fundmen  8960  nqerf  10828  uzrdgfni  13867  hashfun  14346  reltrclfv  14926  homarel  17945  relxpchom  18089  nfchnd  18519  ustrel  24128  utop2nei  24166  utop3cls  24167  metustrel  24468  pi1xfrcnv  24985  reldv  25799  dvbsss  25831  ssrelf  32600  1stpreimas  32691  fpwrelmap  32720  gsumhashmul  33048  metideq  33927  metider  33928  pstmfval  33930  esum2d  34127  txprel  35942  relsset  35951  elfuns  35978  fnsingle  35982  funimage  35991  bj-opelrelex  37209  bj-elid5  37234  mblfinlem1  37717  rngosn3  37984  xrnrel  38426  elrelsrel  38486  dihvalrel  41398  cnvcnvintabd  43717  cnvintabd  43720  clcnvlem  43740  rfovcnvf1od  44121  relopabVD  45017  sprsymrelfo  47621  dmtposss  49000  oppff1  49273  fuco2eld2  49439  fuco22a  49475