Definition df-rel 5595

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 6095 and dfrel3 6104. (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 5593	. 2 wff Rel 𝐴
3		cvv 3431	. . . 4 class V
4	3, 3	cxp 5586	. . 3 class (V × V)
5	1, 4	wss 3886	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 205	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  relxp  5606  pwvrel  5636  brrelex12  5638  0nelrel0  5646  releq  5686  nfrel  5689  sbcrel  5690  relss  5691  ssrel  5692  ssrelOLD  5693  elrel  5708  rel0  5709  nrelv  5710  relsng  5711  relun  5721  reliun  5726  reliin  5727  relopabiv  5730  relopabi  5732  relopabiALT  5733  exopxfr2  5754  relop  5760  eqbrrdva  5779  elreldm  5845  cnvcnv  6098  relrelss  6178  cnviin  6191  dff3  6983  oprabss  7388  relmptopab  7526  1st2nd  7887  1stdm  7888  releldm2  7891  relmpoopab  7941  reldmtpos  8057  dmtpos  8061  dftpos4  8068  tpostpos  8069  iiner  8585  fundmen  8828  nqerf  10693  uzrdgfni  13685  hashfun  14159  reltrclfv  14735  homarel  17758  relxpchom  17905  ustrel  23370  utop2nei  23409  utop3cls  23410  metustrel  23715  pi1xfrcnv  24227  reldv  25041  dvbsss  25073  ssrelf  30962  1stpreimas  31045  fpwrelmap  31075  gsumhashmul  31323  metideq  31850  metider  31851  pstmfval  31853  esum2d  32068  txprel  34188  relsset  34197  elfuns  34224  fnsingle  34228  funimage  34237  bj-opelrelex  35322  bj-elid5  35347  mblfinlem1  35821  rngosn3  36089  xrnrel  36508  elrelsrel  36610  dihvalrel  39298  cnvcnvintabd  41213  cnvintabd  41216  clcnvlem  41236  rfovcnvf1od  41617  relopabVD  42526  sprsymrelfo  44970