Definition df-rel 5623

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

This definition is referenced by:  relxp  5634  pwvrel  5666  brrelex12  5668  0nelrel0  5676  releq  5717  nfrel  5720  sbcrel  5721  relss  5722  ssrel  5723  elrel  5738  rel0  5739  nrelv  5740  relsng  5741  relun  5751  reliun  5756  reliin  5757  relopabiv  5760  relopabi  5762  relopabiALT  5763  exopxfr2  5784  relop  5790  eqbrrdva  5809  elreldm  5875  cnvcnv  6139  relrelss  6220  cnviin  6233  dff3  7033  oprabss  7454  relmptopab  7596  1st2nd  7971  1stdm  7972  releldm2  7975  relmpoopab  8024  reldmtpos  8164  dmtpos  8168  dftpos4  8175  tpostpos  8176  iiner  8713  fundmen  8953  nqerf  10818  uzrdgfni  13862  hashfun  14341  reltrclfv  14921  homarel  17940  relxpchom  18084  nfchnd  18514  ustrel  24125  utop2nei  24163  utop3cls  24164  metustrel  24465  pi1xfrcnv  24982  reldv  25796  dvbsss  25828  ssrelf  32593  1stpreimas  32682  fpwrelmap  32711  gsumhashmul  33036  metideq  33901  metider  33902  pstmfval  33904  esum2d  34101  txprel  35912  relsset  35921  elfuns  35948  fnsingle  35952  funimage  35961  bj-opelrelex  37177  bj-elid5  37202  mblfinlem1  37696  rngosn3  37963  xrnrel  38400  elrelsrel  38523  dihvalrel  41317  cnvcnvintabd  43632  cnvintabd  43635  clcnvlem  43655  rfovcnvf1od  44036  relopabVD  44932  sprsymrelfo  47527  dmtposss  48906  oppff1  49179  fuco2eld2  49345  fuco22a  49381