Definition df-rel 5667

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 5665	. 2 wff Rel 𝐴
3		cvv 3454	. . . 4 class V
4	3, 3	cxp 5658	. . 3 class (V × V)
5	1, 4	wss 3904	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 209	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is used by:  relxp  5678  pwvrel  5710  brrelex12  5712  0nelrel0  5720  releq  5762  nfrel  5765  sbcrel  5766  relss  5767  ssrel  5768  elrel  5783  rel0  5784  nrelvOLD  5786  relsng  5787  relun  5797  reliun  5802  reliin  5803  relopabiv  5806  relopabi  5808  relopabiALT  5809  exopxfr2  5829  relop  5835  eqbrrdva  5854  elreldm  5924  cnvcnv  6189  relrelss  6274  cnviin  6287  dff3  7095  oprabss  7520  relmptopab  7662  1st2nd  8034  1stdm  8035  releldm2  8038  relmpoopab  8087  reldmtpos  8228  dmtpos  8232  dftpos4  8239  tpostpos  8240  iiner  8785  fundmen  9026  nqerf  10921  uzrdgfni  14001  hashfun  14481  reltrclfv  15061  homarel  18099  relxpchom  18243  nfchnd  18673  ustrel  24380  utop2nei  24418  utop3cls  24419  metustrel  24720  pi1xfrcnv  25227  reldv  26040  dvbsss  26072  ssrelf  32971  1stpreimas  33062  fpwrelmap  33089  gsumhashmul  33396  metideq  34292  metider  34293  pstmfval  34295  esum2d  34492  txprel  36377  relsset  36386  elfuns  36413  fnsingle  36417  funimage  36426  bj-opelrelex  37816  bj-elid5  37841  mblfinlem1  38336  rngosn3  38603  xrnrel  39059  elrelsrel  39119  dihvalrel  42081  cnvcnvintabd  44354  cnvintabd  44357  clcnvlem  44377  rfovcnvf1od  44758  relopabVD  45637  sprsymrelfo  48274  dmtposss  49682  oppff1  49954  fuco2eld2  50120  fuco22a  50156