Definition df-rel 5630

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

This definition is referenced by:  relxp  5641  pwvrel  5673  brrelex12  5675  0nelrel0  5683  releq  5724  nfrel  5727  sbcrel  5728  relss  5729  ssrel  5730  elrel  5745  rel0  5746  nrelv  5747  relsng  5748  relun  5758  reliun  5763  reliin  5764  relopabiv  5767  relopabi  5769  relopabiALT  5770  exopxfr2  5791  relop  5797  eqbrrdva  5816  elreldm  5881  cnvcnv  6145  relrelss  6225  cnviin  6238  dff3  7038  oprabss  7461  relmptopab  7603  1st2nd  7981  1stdm  7982  releldm2  7985  relmpoopab  8034  reldmtpos  8174  dmtpos  8178  dftpos4  8185  tpostpos  8186  iiner  8723  fundmen  8963  nqerf  10843  uzrdgfni  13883  hashfun  14362  reltrclfv  14942  homarel  17961  relxpchom  18105  ustrel  24115  utop2nei  24154  utop3cls  24155  metustrel  24456  pi1xfrcnv  24973  reldv  25787  dvbsss  25819  ssrelf  32576  1stpreimas  32662  fpwrelmap  32689  gsumhashmul  33027  metideq  33859  metider  33860  pstmfval  33862  esum2d  34059  txprel  35852  relsset  35861  elfuns  35888  fnsingle  35892  funimage  35901  bj-opelrelex  37117  bj-elid5  37142  mblfinlem1  37636  rngosn3  37903  xrnrel  38340  elrelsrel  38463  dihvalrel  41258  cnvcnvintabd  43573  cnvintabd  43576  clcnvlem  43596  rfovcnvf1od  43977  relopabVD  44874  sprsymrelfo  47482  dmtposss  48861  oppff1  49134  fuco2eld2  49300  fuco22a  49336