Definition df-rel 5121

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5583 and dfrel3 5592. (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 5119	. 2 wff Rel 𝐴
3		cvv 3200	. . . 4 class V
4	3, 3	cxp 5112	. . 3 class (V × V)
5	1, 4	wss 3574	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 196	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  brrelex12  5155  0nelrel  5162  releq  5201  nfrel  5204  sbcrel  5205  relss  5206  ssrel  5207  ssrelOLD  5208  elrel  5222  relsn  5223  relxp  5227  relun  5235  reliun  5239  reliin  5240  rel0  5243  nrelv  5244  relopabi  5245  relopabiALT  5246  exopxfr2  5266  relop  5272  eqbrrdva  5291  elreldm  5350  issref  5509  cnvcnv  5586  cnvcnvOLD  5587  relrelss  5659  cnviin  5672  nfunv  5921  dff3  6372  oprabss  6746  relmptopab  6883  1st2nd  7214  1stdm  7215  releldm2  7218  relmpt2opab  7259  reldmtpos  7360  dmtpos  7364  dftpos4  7371  tpostpos  7372  iiner  7819  fundmen  8030  nqerf  9752  uzrdgfni  12757  hashfun  13224  reltrclfv  13758  homarel  16686  relxpchom  16821  ustrel  22015  utop2nei  22054  utop3cls  22055  metustrel  22357  pi1xfrcnv  22857  reldv  23634  dvbsss  23666  vcex  27433  ssrelf  29425  1stpreimas  29483  fpwrelmap  29508  metideq  29936  metider  29937  pstmfval  29939  esum2d  30155  txprel  31986  relsset  31995  elfuns  32022  fnsingle  32026  funimage  32035  bj-elid  33085  mblfinlem1  33446  rngosn3  33723  xrnrel  34136  dihvalrel  36568  relintabex  37887  cnvcnvintabd  37906  cnvintabd  37909  clcnvlem  37930  rfovcnvf1od  38298  relopabVD  39137  sprsymrelfo  41747