Definition df-rel 5621

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

This definition is referenced by:  relxp  5632  pwvrel  5664  brrelex12  5666  0nelrel0  5674  releq  5716  nfrel  5719  sbcrel  5720  relss  5721  ssrel  5722  elrel  5737  rel0  5738  nrelv  5739  relsng  5740  relun  5750  reliun  5755  reliin  5756  relopabiv  5759  relopabi  5761  relopabiALT  5762  exopxfr2  5783  relop  5789  eqbrrdva  5808  elreldm  5874  cnvcnv  6139  relrelss  6220  cnviin  6233  dff3  7033  oprabss  7454  relmptopab  7596  1st2nd  7971  1stdm  7972  releldm2  7975  relmpoopab  8024  reldmtpos  8164  dmtpos  8168  dftpos4  8175  tpostpos  8176  iiner  8713  fundmen  8953  nqerf  10821  uzrdgfni  13865  hashfun  14344  reltrclfv  14924  homarel  17943  relxpchom  18087  nfchnd  18517  ustrel  24127  utop2nei  24165  utop3cls  24166  metustrel  24467  pi1xfrcnv  24984  reldv  25798  dvbsss  25830  ssrelf  32598  1stpreimas  32687  fpwrelmap  32716  gsumhashmul  33041  metideq  33906  metider  33907  pstmfval  33909  esum2d  34106  txprel  35921  relsset  35930  elfuns  35957  fnsingle  35961  funimage  35970  bj-opelrelex  37188  bj-elid5  37213  mblfinlem1  37696  rngosn3  37963  xrnrel  38405  elrelsrel  38465  dihvalrel  41377  cnvcnvintabd  43692  cnvintabd  43695  clcnvlem  43715  rfovcnvf1od  44096  relopabVD  44992  sprsymrelfo  47596  dmtposss  48975  oppff1  49248  fuco2eld2  49414  fuco22a  49450