Definition df-rel 5657

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

This definition is used by:  relxp  5668  pwvrel  5700  brrelex12  5702  0nelrel0  5710  releq  5752  nfrel  5755  sbcrel  5756  relss  5757  ssrel  5758  elrel  5773  rel0  5775  nrelvOLD  5777  relsng  5778  relun  5788  reliun  5793  reliin  5794  relopabiv  5797  relopabi  5799  relopabiALT  5800  exopxfr2  5821  relop  5827  eqbrrdva  5846  elreldm  5916  cnvcnv  6183  relrelss  6275  cnviin  6289  dff3  7100  oprabss  7528  relmptopab  7671  1st2nd  8050  1stdm  8051  releldm2  8054  relmpoopab  8105  reldmtpos  8251  dmtpos  8255  dftpos4  8262  tpostpos  8263  iiner  8810  fundmen  9059  nqerf  11015  uzrdgfni  14101  hashfun  14582  reltrclfv  15170  homarel  18211  relxpchom  18355  nfchnd  18785  ustrel  24531  utop2nei  24569  utop3cls  24570  metustrel  24871  pi1xfrcnv  25378  reldv  26190  dvbsss  26222  ssrelf  33251  1stpreimas  33341  fpwrelmap  33367  gsumhashmul  33670  metideq  34567  metider  34568  pstmfval  34570  esum2d  34767  txprel  36683  relsset  36692  elfuns  36719  fnsingle  36723  funimage  36732  bj-opelrelex  38108  bj-elid5  38133  mblfinlem1  38618  rngosn3  38901  xrnrel  39357  elrelsrel  39417  dihvalrel  42379  cnvcnvintabd  44642  cnvintabd  44645  clcnvlem  44665  rfovcnvf1od  45046  relopabVD  45925  sprsymrelfo  48621  dmtposss  50026  oppff1  50298  fuco2eld2  50464  fuco22a  50500