Definition df-rel 5587

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

This definition is referenced by:  relxp  5598  pwvrel  5628  brrelex12  5630  0nelrel0  5638  releq  5677  nfrel  5680  sbcrel  5681  relss  5682  ssrel  5683  elrel  5697  rel0  5698  nrelv  5699  relsng  5700  relun  5710  reliun  5715  reliin  5716  relopabiv  5719  relopabi  5721  relopabiALT  5722  exopxfr2  5742  relop  5748  eqbrrdva  5767  elreldm  5833  cnvcnv  6084  relrelss  6165  cnviin  6178  dff3  6958  oprabss  7359  relmptopab  7497  1st2nd  7853  1stdm  7854  releldm2  7857  relmpoopab  7905  reldmtpos  8021  dmtpos  8025  dftpos4  8032  tpostpos  8033  iiner  8536  fundmen  8775  nqerf  10617  uzrdgfni  13606  hashfun  14080  reltrclfv  14656  homarel  17667  relxpchom  17814  ustrel  23271  utop2nei  23310  utop3cls  23311  metustrel  23614  pi1xfrcnv  24126  reldv  24939  dvbsss  24971  ssrelf  30856  1stpreimas  30940  fpwrelmap  30970  gsumhashmul  31218  metideq  31745  metider  31746  pstmfval  31748  esum2d  31961  txprel  34108  relsset  34117  elfuns  34144  fnsingle  34148  funimage  34157  bj-opelrelex  35242  bj-elid5  35267  mblfinlem1  35741  rngosn3  36009  xrnrel  36430  elrelsrel  36532  dihvalrel  39220  cnvcnvintabd  41097  cnvintabd  41100  clcnvlem  41120  rfovcnvf1od  41501  relopabVD  42410  sprsymrelfo  44837