Definition df-rel 5692

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

This definition is referenced by:  relxp  5703  pwvrel  5735  brrelex12  5737  0nelrel0  5745  releq  5786  nfrel  5789  sbcrel  5790  relss  5791  ssrel  5792  ssrelOLD  5793  elrel  5808  rel0  5809  nrelv  5810  relsng  5811  relun  5821  reliun  5826  reliin  5827  relopabiv  5830  relopabi  5832  relopabiALT  5833  exopxfr2  5855  relop  5861  eqbrrdva  5880  elreldm  5946  cnvcnv  6212  relrelss  6293  cnviin  6306  dff3  7120  oprabss  7541  relmptopab  7683  1st2nd  8064  1stdm  8065  releldm2  8068  relmpoopab  8119  reldmtpos  8259  dmtpos  8263  dftpos4  8270  tpostpos  8271  iiner  8829  fundmen  9071  nqerf  10970  uzrdgfni  13999  hashfun  14476  reltrclfv  15056  homarel  18081  relxpchom  18226  ustrel  24220  utop2nei  24259  utop3cls  24260  metustrel  24565  pi1xfrcnv  25090  reldv  25905  dvbsss  25937  ssrelf  32627  1stpreimas  32715  fpwrelmap  32744  gsumhashmul  33064  metideq  33892  metider  33893  pstmfval  33895  esum2d  34094  txprel  35880  relsset  35889  elfuns  35916  fnsingle  35920  funimage  35929  bj-opelrelex  37145  bj-elid5  37170  mblfinlem1  37664  rngosn3  37931  xrnrel  38374  elrelsrel  38488  dihvalrel  41281  cnvcnvintabd  43613  cnvintabd  43616  clcnvlem  43636  rfovcnvf1od  44017  relopabVD  44921  sprsymrelfo  47484  dmtposss  48776  fuco2eld2  49009  fuco22a  49045