Definition df-rel 5562

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 6046 and dfrel3 6055. (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 5560	. 2 wff Rel 𝐴
3		cvv 3494	. . . 4 class V
4	3, 3	cxp 5553	. . 3 class (V × V)
5	1, 4	wss 3936	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 208	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  relxp  5573  pwvrel  5602  brrelex12  5604  0nelrel0  5612  releq  5651  nfrel  5654  sbcrel  5655  relss  5656  ssrel  5657  elrel  5671  rel0  5672  nrelv  5673  relsng  5674  relun  5684  reliun  5689  reliin  5690  relopabiv  5693  relopabi  5694  relopabiALT  5695  exopxfr2  5715  relop  5721  eqbrrdva  5740  elreldm  5805  cnvcnv  6049  relrelss  6124  cnviin  6137  dff3  6866  oprabss  7260  relmptopab  7395  1st2nd  7738  1stdm  7739  releldm2  7742  relmpoopab  7789  reldmtpos  7900  dmtpos  7904  dftpos4  7911  tpostpos  7912  iiner  8369  fundmen  8583  nqerf  10352  uzrdgfni  13327  hashfun  13799  reltrclfv  14377  homarel  17296  relxpchom  17431  ustrel  22820  utop2nei  22859  utop3cls  22860  metustrel  23162  pi1xfrcnv  23661  reldv  24468  dvbsss  24500  ssrelf  30366  1stpreimas  30441  fpwrelmap  30469  metideq  31133  metider  31134  pstmfval  31136  esum2d  31352  txprel  33340  relsset  33349  elfuns  33376  fnsingle  33380  funimage  33389  bj-opelrelex  34439  bj-elid5  34464  mblfinlem1  34944  rngosn3  35217  xrnrel  35640  elrelsrel  35742  dihvalrel  38430  cnvcnvintabd  40009  cnvintabd  40012  clcnvlem  40032  rfovcnvf1od  40399  relopabVD  41284  sprsymrelfo  43708