Definition df-rel 5654

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

This definition is used by:  relxp  5665  pwvrel  5697  brrelex12  5699  0nelrel0  5707  releq  5749  nfrel  5752  sbcrel  5753  relss  5754  ssrel  5755  elrel  5770  rel0  5772  nrelvOLD  5774  relsng  5775  relun  5785  reliun  5790  reliin  5791  relopabiv  5794  relopabi  5796  relopabiALT  5797  exopxfr2  5818  relop  5824  eqbrrdva  5843  elreldm  5913  cnvcnv  6179  relrelss  6264  cnviin  6278  dff3  7088  oprabss  7516  relmptopab  7659  1st2nd  8033  1stdm  8034  releldm2  8037  relmpoopab  8088  reldmtpos  8229  dmtpos  8233  dftpos4  8240  tpostpos  8241  iiner  8788  fundmen  9037  nqerf  10986  uzrdgfni  14069  hashfun  14549  reltrclfv  15137  homarel  18172  relxpchom  18316  nfchnd  18746  ustrel  24492  utop2nei  24530  utop3cls  24531  metustrel  24832  pi1xfrcnv  25339  reldv  26151  dvbsss  26183  ssrelf  33142  1stpreimas  33232  fpwrelmap  33258  gsumhashmul  33561  metideq  34458  metider  34459  pstmfval  34461  esum2d  34658  txprel  36563  relsset  36572  elfuns  36599  fnsingle  36603  funimage  36612  bj-opelrelex  37985  bj-elid5  38010  mblfinlem1  38495  rngosn3  38778  xrnrel  39234  elrelsrel  39294  dihvalrel  42256  cnvcnvintabd  44544  cnvintabd  44547  clcnvlem  44567  rfovcnvf1od  44948  relopabVD  45827  sprsymrelfo  48501  dmtposss  49906  oppff1  50178  fuco2eld2  50344  fuco22a  50380