Definition df-rel 5591

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

This definition is referenced by:  relxp  5602  pwvrel  5632  brrelex12  5634  0nelrel0  5642  releq  5681  nfrel  5684  sbcrel  5685  relss  5686  ssrel  5687  elrel  5701  rel0  5702  nrelv  5703  relsng  5704  relun  5714  reliun  5719  reliin  5720  relopabiv  5723  relopabi  5725  relopabiALT  5726  exopxfr2  5746  relop  5752  eqbrrdva  5771  elreldm  5837  cnvcnv  6088  relrelss  6169  cnviin  6182  dff3  6968  oprabss  7371  relmptopab  7509  1st2nd  7869  1stdm  7870  releldm2  7873  relmpoopab  7921  reldmtpos  8037  dmtpos  8041  dftpos4  8048  tpostpos  8049  iiner  8565  fundmen  8808  nqerf  10696  uzrdgfni  13688  hashfun  14162  reltrclfv  14738  homarel  17761  relxpchom  17908  ustrel  23373  utop2nei  23412  utop3cls  23413  metustrel  23718  pi1xfrcnv  24230  reldv  25044  dvbsss  25076  ssrelf  30963  1stpreimas  31046  fpwrelmap  31076  gsumhashmul  31324  metideq  31851  metider  31852  pstmfval  31854  esum2d  32069  txprel  34189  relsset  34198  elfuns  34225  fnsingle  34229  funimage  34238  bj-opelrelex  35323  bj-elid5  35348  mblfinlem1  35822  rngosn3  36090  xrnrel  36511  elrelsrel  36613  dihvalrel  39301  cnvcnvintabd  41189  cnvintabd  41192  clcnvlem  41212  rfovcnvf1od  41593  relopabVD  42502  sprsymrelfo  44927