Definition df-rel 5695

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

This definition is referenced by:  relxp  5706  pwvrel  5738  brrelex12  5740  0nelrel0  5748  releq  5788  nfrel  5791  sbcrel  5792  relss  5793  ssrel  5794  ssrelOLD  5795  elrel  5810  rel0  5811  nrelv  5812  relsng  5813  relun  5823  reliun  5828  reliin  5829  relopabiv  5832  relopabi  5834  relopabiALT  5835  exopxfr2  5857  relop  5863  eqbrrdva  5882  elreldm  5948  cnvcnv  6213  relrelss  6294  cnviin  6307  dff3  7119  oprabss  7539  relmptopab  7682  1st2nd  8062  1stdm  8063  releldm2  8066  relmpoopab  8117  reldmtpos  8257  dmtpos  8261  dftpos4  8268  tpostpos  8269  iiner  8827  fundmen  9069  nqerf  10967  uzrdgfni  13995  hashfun  14472  reltrclfv  15052  homarel  18089  relxpchom  18236  ustrel  24235  utop2nei  24274  utop3cls  24275  metustrel  24580  pi1xfrcnv  25103  reldv  25919  dvbsss  25951  ssrelf  32634  1stpreimas  32720  fpwrelmap  32750  gsumhashmul  33046  metideq  33853  metider  33854  pstmfval  33856  esum2d  34073  txprel  35860  relsset  35869  elfuns  35896  fnsingle  35900  funimage  35909  bj-opelrelex  37126  bj-elid5  37151  mblfinlem1  37643  rngosn3  37910  xrnrel  38354  elrelsrel  38468  dihvalrel  41261  cnvcnvintabd  43589  cnvintabd  43592  clcnvlem  43612  rfovcnvf1od  43993  relopabVD  44898  sprsymrelfo  47421