Definition df-rel 5635

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

This definition is referenced by:  relxp  5646  pwvrel  5678  brrelex12  5680  0nelrel0  5688  releq  5730  nfrel  5733  sbcrel  5734  relss  5735  ssrel  5736  elrel  5751  rel0  5752  nrelv  5753  relsng  5754  relun  5764  reliun  5769  reliin  5770  relopabiv  5773  relopabi  5775  relopabiALT  5776  exopxfr2  5797  relop  5803  eqbrrdva  5822  elreldm  5888  cnvcnv  6154  relrelss  6235  cnviin  6248  dff3  7050  oprabss  7472  relmptopab  7614  1st2nd  7989  1stdm  7990  releldm2  7993  relmpoopab  8041  reldmtpos  8181  dmtpos  8185  dftpos4  8192  tpostpos  8193  iiner  8733  fundmen  8975  nqerf  10850  uzrdgfni  13917  hashfun  14396  reltrclfv  14976  homarel  18000  relxpchom  18144  nfchnd  18574  ustrel  24174  utop2nei  24212  utop3cls  24213  metustrel  24514  pi1xfrcnv  25021  reldv  25834  dvbsss  25866  ssrelf  32685  1stpreimas  32776  fpwrelmap  32803  gsumhashmul  33125  metideq  34034  metider  34035  pstmfval  34037  esum2d  34234  txprel  36056  relsset  36065  elfuns  36092  fnsingle  36096  funimage  36105  bj-opelrelex  37455  bj-elid5  37480  mblfinlem1  37975  rngosn3  38242  xrnrel  38700  elrelsrel  38760  dihvalrel  41722  cnvcnvintabd  44024  cnvintabd  44027  clcnvlem  44047  rfovcnvf1od  44428  relopabVD  45324  sprsymrelfo  47948  dmtposss  49342  oppff1  49614  fuco2eld2  49780  fuco22a  49816