Definition df-rel 5668

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

This definition is referenced by:  relxp  5679  pwvrel  5711  brrelex12  5713  0nelrel0  5721  releq  5763  nfrel  5766  sbcrel  5767  relss  5768  ssrel  5769  elrel  5784  rel0  5785  nrelvOLD  5787  relsng  5788  relun  5798  reliun  5803  reliin  5804  relopabiv  5807  relopabi  5809  relopabiALT  5810  exopxfr2  5830  relop  5836  eqbrrdva  5855  elreldm  5925  cnvcnv  6190  relrelss  6274  cnviin  6287  dff3  7095  oprabss  7518  relmptopab  7660  1st2nd  8035  1stdm  8036  releldm2  8039  relmpoopab  8088  reldmtpos  8229  dmtpos  8233  dftpos4  8240  tpostpos  8241  iiner  8786  fundmen  9027  nqerf  10914  uzrdgfni  13993  hashfun  14473  reltrclfv  15053  homarel  18092  relxpchom  18236  nfchnd  18666  ustrel  24348  utop2nei  24386  utop3cls  24387  metustrel  24688  pi1xfrcnv  25195  reldv  26008  dvbsss  26040  ssrelf  32926  1stpreimas  33017  fpwrelmap  33044  gsumhashmul  33353  metideq  34249  metider  34250  pstmfval  34252  esum2d  34449  txprel  36323  relsset  36332  elfuns  36359  fnsingle  36363  funimage  36372  bj-opelrelex  37732  bj-elid5  37757  mblfinlem1  38252  rngosn3  38519  xrnrel  38977  elrelsrel  39037  dihvalrel  41999  cnvcnvintabd  44274  cnvintabd  44277  clcnvlem  44297  rfovcnvf1od  44678  relopabVD  45557  sprsymrelfo  48191  dmtposss  49599  oppff1  49871  fuco2eld2  50037  fuco22a  50073