Definition df-rel 5683

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

This definition is referenced by:  relxp  5694  pwvrel  5725  brrelex12  5727  0nelrel0  5735  releq  5775  nfrel  5778  sbcrel  5779  relss  5780  ssrel  5781  ssrelOLD  5782  elrel  5797  rel0  5798  nrelv  5799  relsng  5800  relun  5810  reliun  5815  reliin  5816  relopabiv  5819  relopabi  5821  relopabiALT  5822  exopxfr2  5843  relop  5849  eqbrrdva  5868  elreldm  5933  cnvcnv  6189  relrelss  6270  cnviin  6283  dff3  7099  oprabss  7512  relmptopab  7653  1st2nd  8022  1stdm  8023  releldm2  8026  relmpoopab  8077  reldmtpos  8216  dmtpos  8220  dftpos4  8227  tpostpos  8228  iiner  8780  fundmen  9028  nqerf  10922  uzrdgfni  13920  hashfun  14394  reltrclfv  14961  homarel  17983  relxpchom  18130  ustrel  23708  utop2nei  23747  utop3cls  23748  metustrel  24053  pi1xfrcnv  24565  reldv  25379  dvbsss  25411  ssrelf  31832  1stpreimas  31915  fpwrelmap  31946  gsumhashmul  32196  metideq  32862  metider  32863  pstmfval  32865  esum2d  33080  txprel  34840  relsset  34849  elfuns  34876  fnsingle  34880  funimage  34889  bj-opelrelex  36014  bj-elid5  36039  mblfinlem1  36514  rngosn3  36781  xrnrel  37232  elrelsrel  37346  dihvalrel  40139  cnvcnvintabd  42337  cnvintabd  42340  clcnvlem  42360  rfovcnvf1od  42741  relopabVD  43648  sprsymrelfo  46152