Definition df-rel 5666

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

This definition is used by:  relxp  5677  pwvrel  5709  brrelex12  5711  0nelrel0  5719  releq  5761  nfrel  5764  sbcrel  5765  relss  5766  ssrel  5767  elrel  5782  rel0  5783  nrelvOLD  5785  relsng  5786  relun  5796  reliun  5801  reliin  5802  relopabiv  5805  relopabi  5807  relopabiALT  5808  exopxfr2  5828  relop  5834  eqbrrdva  5853  elreldm  5923  cnvcnv  6189  relrelss  6274  cnviin  6288  dff3  7096  oprabss  7524  relmptopab  7667  1st2nd  8039  1stdm  8040  releldm2  8043  relmpoopab  8094  reldmtpos  8235  dmtpos  8239  dftpos4  8246  tpostpos  8247  iiner  8792  fundmen  9041  nqerf  10942  uzrdgfni  14024  hashfun  14504  reltrclfv  15092  homarel  18129  relxpchom  18273  nfchnd  18703  ustrel  24439  utop2nei  24477  utop3cls  24478  metustrel  24779  pi1xfrcnv  25286  reldv  26099  dvbsss  26131  ssrelf  33075  1stpreimas  33165  fpwrelmap  33191  gsumhashmul  33494  metideq  34390  metider  34391  pstmfval  34393  esum2d  34590  txprel  36443  relsset  36452  elfuns  36479  fnsingle  36483  funimage  36492  bj-opelrelex  37883  bj-elid5  37908  mblfinlem1  38393  rngosn3  38661  xrnrel  39117  elrelsrel  39177  dihvalrel  42139  cnvcnvintabd  44427  cnvintabd  44430  clcnvlem  44450  rfovcnvf1od  44831  relopabVD  45710  sprsymrelfo  48384  dmtposss  49789  oppff1  50061  fuco2eld2  50227  fuco22a  50263