Definition df-rel 5318

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5794 and dfrel3 5803. (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 5316	. 2 wff Rel 𝐴
3		cvv 3391	. . . 4 class V
4	3, 3	cxp 5309	. . 3 class (V × V)
5	1, 4	wss 3769	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 197	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  relxp  5328  brrelex12  5355  0nelrel  5362  releq  5403  nfrel  5406  sbcrel  5407  relss  5408  ssrel  5409  ssrelOLD  5410  elrel  5424  relsng  5425  relsnOLD  5428  relun  5436  reliun  5441  reliin  5442  rel0  5445  nrelv  5446  relopabi  5447  relopabiALT  5448  exopxfr2  5468  relop  5474  eqbrrdva  5493  elreldm  5551  idrefOLD  5720  cnvcnv  5797  cnvcnvOLD  5798  relrelss  5873  cnviin  5886  nfunv  6130  dff3  6590  oprabss  6972  relmptopab  7109  1st2nd  7442  1stdm  7443  releldm2  7446  relmpt2opab  7489  reldmtpos  7591  dmtpos  7595  dftpos4  7602  tpostpos  7603  iiner  8050  fundmen  8262  nqerf  10033  uzrdgfni  12977  hashfun  13437  reltrclfv  13977  homarel  16886  relxpchom  17022  ustrel  22224  utop2nei  22263  utop3cls  22264  metustrel  22566  pi1xfrcnv  23065  reldv  23844  dvbsss  23876  vcex  27757  ssrelf  29748  1stpreimas  29806  fpwrelmap  29831  metideq  30257  metider  30258  pstmfval  30260  esum2d  30476  txprel  32302  relsset  32311  elfuns  32338  fnsingle  32342  funimage  32351  bj-elid  33396  mblfinlem1  33754  rngosn3  34029  xrnrel  34443  elrelsrel  34545  dihvalrel  37054  relintabex  38381  cnvcnvintabd  38400  cnvintabd  38403  clcnvlem  38424  rfovcnvf1od  38792  relopabVD  39625  sprsymrelfo  42309