Definition df-rel 5543

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

This definition is referenced by:  relxp  5554  pwvrel  5584  brrelex12  5586  0nelrel0  5594  releq  5633  nfrel  5636  sbcrel  5637  relss  5638  ssrel  5639  elrel  5653  rel0  5654  nrelv  5655  relsng  5656  relun  5666  reliun  5671  reliin  5672  relopabiv  5675  relopabi  5677  relopabiALT  5678  exopxfr2  5698  relop  5704  eqbrrdva  5723  elreldm  5789  cnvcnv  6035  relrelss  6116  cnviin  6129  dff3  6897  oprabss  7295  relmptopab  7433  1st2nd  7788  1stdm  7789  releldm2  7792  relmpoopab  7840  reldmtpos  7954  dmtpos  7958  dftpos4  7965  tpostpos  7966  iiner  8449  fundmen  8686  nqerf  10509  uzrdgfni  13496  hashfun  13969  reltrclfv  14545  homarel  17496  relxpchom  17642  ustrel  23063  utop2nei  23102  utop3cls  23103  metustrel  23404  pi1xfrcnv  23908  reldv  24721  dvbsss  24753  ssrelf  30628  1stpreimas  30712  fpwrelmap  30742  gsumhashmul  30989  metideq  31511  metider  31512  pstmfval  31514  esum2d  31727  txprel  33867  relsset  33876  elfuns  33903  fnsingle  33907  funimage  33916  bj-opelrelex  34999  bj-elid5  35024  mblfinlem1  35500  rngosn3  35768  xrnrel  36189  elrelsrel  36291  dihvalrel  38979  cnvcnvintabd  40825  cnvintabd  40828  clcnvlem  40848  rfovcnvf1od  41230  relopabVD  42135  sprsymrelfo  44565