Definition df-rel 5645

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

This definition is referenced by:  relxp  5656  pwvrel  5688  brrelex12  5690  0nelrel0  5698  releq  5739  nfrel  5742  sbcrel  5743  relss  5744  ssrel  5745  ssrelOLD  5746  elrel  5761  rel0  5762  nrelv  5763  relsng  5764  relun  5774  reliun  5779  reliin  5780  relopabiv  5783  relopabi  5785  relopabiALT  5786  exopxfr2  5808  relop  5814  eqbrrdva  5833  elreldm  5899  cnvcnv  6165  relrelss  6246  cnviin  6259  dff3  7072  oprabss  7497  relmptopab  7639  1st2nd  8018  1stdm  8019  releldm2  8022  relmpoopab  8073  reldmtpos  8213  dmtpos  8217  dftpos4  8224  tpostpos  8225  iiner  8762  fundmen  9002  nqerf  10883  uzrdgfni  13923  hashfun  14402  reltrclfv  14983  homarel  17998  relxpchom  18142  ustrel  24099  utop2nei  24138  utop3cls  24139  metustrel  24440  pi1xfrcnv  24957  reldv  25771  dvbsss  25803  ssrelf  32543  1stpreimas  32629  fpwrelmap  32656  gsumhashmul  33001  metideq  33883  metider  33884  pstmfval  33886  esum2d  34083  txprel  35867  relsset  35876  elfuns  35903  fnsingle  35907  funimage  35916  bj-opelrelex  37132  bj-elid5  37157  mblfinlem1  37651  rngosn3  37918  xrnrel  38355  elrelsrel  38478  dihvalrel  41273  cnvcnvintabd  43589  cnvintabd  43592  clcnvlem  43612  rfovcnvf1od  43993  relopabVD  44890  sprsymrelfo  47498  dmtposss  48864  oppff1  49137  fuco2eld2  49303  fuco22a  49339