Definition df-rel 5669

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 6188 and dfrel3 6198. (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 5667	. 2 wff Rel 𝐴
3		cvv 3463	. . . 4 class V
4	3, 3	cxp 5660	. . 3 class (V × V)
5	1, 4	wss 3913	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 209	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  relxp  5680  pwvrel  5712  brrelex12  5714  0nelrel0  5722  releq  5764  nfrel  5767  sbcrel  5768  relss  5769  ssrel  5770  elrel  5785  rel0  5786  nrelvOLD  5788  relsng  5789  relun  5799  reliun  5804  reliin  5805  relopabiv  5808  relopabi  5810  relopabiALT  5811  exopxfr2  5831  relop  5837  eqbrrdva  5856  elreldm  5926  cnvcnv  6191  relrelss  6275  cnviin  6288  dff3  7096  oprabss  7519  relmptopab  7661  1st2nd  8036  1stdm  8037  releldm2  8040  relmpoopab  8089  reldmtpos  8230  dmtpos  8234  dftpos4  8241  tpostpos  8242  iiner  8787  fundmen  9028  nqerf  10915  uzrdgfni  13994  hashfun  14474  reltrclfv  15054  homarel  18093  relxpchom  18237  nfchnd  18667  ustrel  24338  utop2nei  24376  utop3cls  24377  metustrel  24678  pi1xfrcnv  25185  reldv  25998  dvbsss  26030  ssrelf  32901  1stpreimas  32992  fpwrelmap  33019  gsumhashmul  33328  metideq  34228  metider  34229  pstmfval  34231  esum2d  34428  txprel  36268  relsset  36277  elfuns  36304  fnsingle  36308  funimage  36317  bj-opelrelex  37676  bj-elid5  37701  mblfinlem1  38196  rngosn3  38463  xrnrel  38921  elrelsrel  38981  dihvalrel  41943  cnvcnvintabd  44218  cnvintabd  44221  clcnvlem  44241  rfovcnvf1od  44622  relopabVD  45501  sprsymrelfo  48135  dmtposss  49539  oppff1  49811  fuco2eld2  49977  fuco22a  50013