Definition df-rel 5707

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

This definition is referenced by:  relxp  5718  pwvrel  5750  brrelex12  5752  0nelrel0  5760  releq  5800  nfrel  5803  sbcrel  5804  relss  5805  ssrel  5806  ssrelOLD  5807  elrel  5822  rel0  5823  nrelv  5824  relsng  5825  relun  5835  reliun  5840  reliin  5841  relopabiv  5844  relopabi  5846  relopabiALT  5847  exopxfr2  5869  relop  5875  eqbrrdva  5894  elreldm  5960  cnvcnv  6223  relrelss  6304  cnviin  6317  dff3  7134  oprabss  7557  relmptopab  7700  1st2nd  8080  1stdm  8081  releldm2  8084  relmpoopab  8135  reldmtpos  8275  dmtpos  8279  dftpos4  8286  tpostpos  8287  iiner  8847  fundmen  9096  nqerf  10999  uzrdgfni  14009  hashfun  14486  reltrclfv  15066  homarel  18103  relxpchom  18250  ustrel  24241  utop2nei  24280  utop3cls  24281  metustrel  24586  pi1xfrcnv  25109  reldv  25925  dvbsss  25957  ssrelf  32637  1stpreimas  32717  fpwrelmap  32747  gsumhashmul  33040  metideq  33839  metider  33840  pstmfval  33842  esum2d  34057  txprel  35843  relsset  35852  elfuns  35879  fnsingle  35883  funimage  35892  bj-opelrelex  37110  bj-elid5  37135  mblfinlem1  37617  rngosn3  37884  xrnrel  38329  elrelsrel  38443  dihvalrel  41236  cnvcnvintabd  43562  cnvintabd  43565  clcnvlem  43585  rfovcnvf1od  43966  relopabVD  44872  sprsymrelfo  47371