Definition df-rel 5411

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5884 and dfrel3 5892. (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 5409	. 2 wff Rel 𝐴
3		cvv 3412	. . . 4 class V
4	3, 3	cxp 5402	. . 3 class (V × V)
5	1, 4	wss 3828	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 198	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  relxp  5422  brrelex12  5451  0nelrel0  5459  releq  5498  nfrel  5501  sbcrel  5502  relss  5503  ssrel  5504  elrel  5518  rel0  5519  nrelv  5520  relsng  5521  relun  5531  reliun  5536  reliin  5537  relopabiv  5540  relopabi  5541  relopabiALT  5542  exopxfr2  5562  relop  5568  eqbrrdva  5587  elreldm  5645  cnvcnv  5887  relrelss  5960  cnviin  5973  dff3  6687  oprabss  7074  relmptopab  7211  1st2nd  7547  1stdm  7548  releldm2  7551  relmpoopab  7594  reldmtpos  7700  dmtpos  7704  dftpos4  7711  tpostpos  7712  iiner  8165  fundmen  8376  nqerf  10146  uzrdgfni  13138  hashfun  13605  reltrclfv  14232  homarel  17148  relxpchom  17283  ustrel  22517  utop2nei  22556  utop3cls  22557  metustrel  22859  pi1xfrcnv  23358  reldv  24165  dvbsss  24197  ssrelf  30124  1stpreimas  30187  fpwrelmap  30215  metideq  30768  metider  30769  pstmfval  30771  esum2d  30987  txprel  32831  relsset  32840  elfuns  32867  fnsingle  32871  funimage  32880  bj-elid  33903  mblfinlem1  34348  rngosn3  34622  xrnrel  35048  elrelsrel  35150  dihvalrel  37838  relintabex  39281  cnvcnvintabd  39300  cnvintabd  39303  clcnvlem  39324  rfovcnvf1od  39691  relopabVD  40631  sprsymrelfo  43001