Definition df-rel 5662

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

This definition is used by:  relxp  5673  pwvrel  5705  brrelex12  5707  0nelrel0  5715  releq  5758  nfrel  5761  sbcrel  5762  relss  5763  ssrel  5764  elrel  5779  rel0  5781  nrelvOLD  5783  relsng  5784  relun  5794  reliun  5799  reliin  5800  relopabiv  5803  relopabi  5805  relopabiALT  5806  exopxfr2  5827  relop  5833  eqbrrdva  5853  elreldm  5923  cnvcnv  6195  relrelss  6290  cnviin  6304  dff3  7121  oprabss  7548  relmptopab  7692  1st2nd  8071  1stdm  8072  releldm2  8075  relmpoopab  8128  reldmtpos  8276  dmtpos  8280  dftpos4  8287  tpostpos  8288  iiner  8835  fundmen  9084  nqerf  11039  uzrdgfni  14125  hashfun  14606  reltrclfv  15196  homarel  18237  relxpchom  18381  nfchnd  18811  ustrel  24558  utop2nei  24596  utop3cls  24597  metustrel  24898  pi1xfrcnv  25405  reldv  26217  dvbsss  26249  ssrelf  33278  1stpreimas  33367  fpwrelmap  33392  gsumhashmul  33695  metideq  34592  metider  34593  pstmfval  34595  esum2d  34792  txprel  36818  relsset  36827  elfuns  36854  fnsingle  36858  funimage  36867  bj-dfrel3  38143  bj-opelrelex  38256  bj-elid5  38281  mblfinlem1  38766  rngosn3  39049  xrnrel  39505  elrelsrel  39565  dihvalrel  42527  cnvcnvintabd  44790  cnvintabd  44793  clcnvlem  44813  rfovcnvf1od  45194  relopabVD  46072  sprsymrelfo  48782  dmtposss  50192  oppff1  50467  fuco2eld2  50639  fuco22a  50675