Definition df-rel 5661

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

This definition is referenced by:  relxp  5672  pwvrel  5704  brrelex12  5706  0nelrel0  5714  releq  5755  nfrel  5758  sbcrel  5759  relss  5760  ssrel  5761  ssrelOLD  5762  elrel  5777  rel0  5778  nrelv  5779  relsng  5780  relun  5790  reliun  5795  reliin  5796  relopabiv  5799  relopabi  5801  relopabiALT  5802  exopxfr2  5824  relop  5830  eqbrrdva  5849  elreldm  5915  cnvcnv  6181  relrelss  6262  cnviin  6275  dff3  7089  oprabss  7513  relmptopab  7655  1st2nd  8036  1stdm  8037  releldm2  8040  relmpoopab  8091  reldmtpos  8231  dmtpos  8235  dftpos4  8242  tpostpos  8243  iiner  8801  fundmen  9043  nqerf  10942  uzrdgfni  13974  hashfun  14453  reltrclfv  15034  homarel  18047  relxpchom  18191  ustrel  24148  utop2nei  24187  utop3cls  24188  metustrel  24489  pi1xfrcnv  25006  reldv  25821  dvbsss  25853  ssrelf  32541  1stpreimas  32629  fpwrelmap  32656  gsumhashmul  33001  metideq  33870  metider  33871  pstmfval  33873  esum2d  34070  txprel  35843  relsset  35852  elfuns  35879  fnsingle  35883  funimage  35892  bj-opelrelex  37108  bj-elid5  37133  mblfinlem1  37627  rngosn3  37894  xrnrel  38337  elrelsrel  38451  dihvalrel  41244  cnvcnvintabd  43571  cnvintabd  43574  clcnvlem  43594  rfovcnvf1od  43975  relopabVD  44873  sprsymrelfo  47459  dmtposss  48799  fuco2eld2  49173  fuco22a  49209