Definition df-rel 5685

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

This definition is referenced by:  relxp  5696  pwvrel  5728  brrelex12  5730  0nelrel0  5738  releq  5778  nfrel  5781  sbcrel  5782  relss  5783  ssrel  5784  ssrelOLD  5785  elrel  5800  rel0  5801  nrelv  5802  relsng  5803  relun  5813  reliun  5818  reliin  5819  relopabiv  5822  relopabi  5824  relopabiALT  5825  exopxfr2  5847  relop  5853  eqbrrdva  5872  elreldm  5937  cnvcnv  6198  relrelss  6279  cnviin  6292  dff3  7109  oprabss  7527  relmptopab  7671  1st2nd  8044  1stdm  8045  releldm2  8048  relmpoopab  8099  reldmtpos  8240  dmtpos  8244  dftpos4  8251  tpostpos  8252  iiner  8808  fundmen  9056  nqerf  10955  uzrdgfni  13959  hashfun  14432  reltrclfv  15000  homarel  18028  relxpchom  18175  ustrel  24160  utop2nei  24199  utop3cls  24200  metustrel  24505  pi1xfrcnv  25028  reldv  25843  dvbsss  25875  ssrelf  32484  1stpreimas  32567  fpwrelmap  32597  gsumhashmul  32860  metideq  33625  metider  33626  pstmfval  33628  esum2d  33843  txprel  35606  relsset  35615  elfuns  35642  fnsingle  35646  funimage  35655  bj-opelrelex  36754  bj-elid5  36779  mblfinlem1  37261  rngosn3  37528  xrnrel  37975  elrelsrel  38089  dihvalrel  40882  cnvcnvintabd  43172  cnvintabd  43175  clcnvlem  43195  rfovcnvf1od  43576  relopabVD  44482  sprsymrelfo  46974