Definition df-rel 5648

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

This definition is referenced by:  relxp  5659  pwvrel  5691  brrelex12  5693  0nelrel0  5701  releq  5742  nfrel  5745  sbcrel  5746  relss  5747  ssrel  5748  ssrelOLD  5749  elrel  5764  rel0  5765  nrelv  5766  relsng  5767  relun  5777  reliun  5782  reliin  5783  relopabiv  5786  relopabi  5788  relopabiALT  5789  exopxfr2  5811  relop  5817  eqbrrdva  5836  elreldm  5902  cnvcnv  6168  relrelss  6249  cnviin  6262  dff3  7075  oprabss  7500  relmptopab  7642  1st2nd  8021  1stdm  8022  releldm2  8025  relmpoopab  8076  reldmtpos  8216  dmtpos  8220  dftpos4  8227  tpostpos  8228  iiner  8765  fundmen  9005  nqerf  10890  uzrdgfni  13930  hashfun  14409  reltrclfv  14990  homarel  18005  relxpchom  18149  ustrel  24106  utop2nei  24145  utop3cls  24146  metustrel  24447  pi1xfrcnv  24964  reldv  25778  dvbsss  25810  ssrelf  32550  1stpreimas  32636  fpwrelmap  32663  gsumhashmul  33008  metideq  33890  metider  33891  pstmfval  33893  esum2d  34090  txprel  35874  relsset  35883  elfuns  35910  fnsingle  35914  funimage  35923  bj-opelrelex  37139  bj-elid5  37164  mblfinlem1  37658  rngosn3  37925  xrnrel  38362  elrelsrel  38485  dihvalrel  41280  cnvcnvintabd  43596  cnvintabd  43599  clcnvlem  43619  rfovcnvf1od  44000  relopabVD  44897  sprsymrelfo  47502  dmtposss  48868  oppff1  49141  fuco2eld2  49307  fuco22a  49343