Definition df-rel 5627

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 6143 and dfrel3 6152. (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 5625	. 2 wff Rel 𝐴
3		cvv 3433	. . . 4 class V
4	3, 3	cxp 5618	. . 3 class (V × V)
5	1, 4	wss 3884	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 208	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  relxp  5638  pwvrel  5670  brrelex12  5672  0nelrel0  5680  releq  5722  nfrel  5725  sbcrel  5726  relss  5727  ssrel  5728  elrel  5743  rel0  5744  nrelv  5745  relsng  5746  relun  5756  reliun  5761  reliin  5762  relopabiv  5765  relopabi  5767  relopabiALT  5768  exopxfr2  5788  relop  5794  eqbrrdva  5813  elreldm  5883  cnvcnv  6146  relrelss  6227  cnviin  6240  dff3  7044  oprabss  7467  relmptopab  7609  1st2nd  7983  1stdm  7984  releldm2  7987  relmpoopab  8035  reldmtpos  8176  dmtpos  8180  dftpos4  8187  tpostpos  8188  iiner  8730  fundmen  8972  nqerf  10849  uzrdgfni  13915  hashfun  14394  reltrclfv  14974  homarel  17998  relxpchom  18142  nfchnd  18572  ustrel  24198  utop2nei  24236  utop3cls  24237  metustrel  24538  pi1xfrcnv  25045  reldv  25858  dvbsss  25890  ssrelf  32709  1stpreimas  32800  fpwrelmap  32827  gsumhashmul  33150  metideq  34087  metider  34088  pstmfval  34090  esum2d  34287  txprel  36118  relsset  36127  elfuns  36154  fnsingle  36158  funimage  36167  bj-opelrelex  37517  bj-elid5  37542  mblfinlem1  38037  rngosn3  38304  xrnrel  38762  elrelsrel  38822  dihvalrel  41784  cnvcnvintabd  44057  cnvintabd  44060  clcnvlem  44080  rfovcnvf1od  44461  relopabVD  45357  sprsymrelfo  47984  dmtposss  49378  oppff1  49650  fuco2eld2  49816  fuco22a  49852