Definition df-rel 5045

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5502 and dfrel3 5510. (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 5043	. 2 wff Rel 𝐴
3		cvv 3173	. . . 4 class V
4	3, 3	cxp 5036	. . 3 class (V × V)
5	1, 4	wss 3540	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 195	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  brrelex12  5079  releq  5124  nfrel  5127  sbcrel  5128  relss  5129  ssrel  5130  ssrelOLD  5131  elrel  5145  relsn  5146  relxp  5150  relun  5158  reliun  5162  reliin  5163  rel0  5166  relopabi  5167  relopabiALT  5168  exopxfr2  5188  relop  5194  eqbrrdva  5213  elreldm  5271  issref  5428  cnvcnv  5505  relrelss  5576  cnviin  5589  nfunv  5835  dff3  6280  oprabss  6644  relmptopab  6781  1st2nd  7105  1stdm  7106  releldm2  7109  relmpt2opab  7146  reldmtpos  7247  dmtpos  7251  dftpos4  7258  tpostpos  7259  iiner  7706  fundmen  7916  nqerf  9631  uzrdgfni  12619  hashfun  13084  reltrclfv  13606  homarel  16509  relxpchom  16644  ustrel  21825  utop2nei  21864  utop3cls  21865  metustrel  22167  pi1xfrcnv  22665  reldv  23440  dvbsss  23472  uhgraopelvv  25826  vcex  26817  ssrelf  28805  1stpreimas  28866  fpwrelmap  28896  metideq  29264  metider  29265  pstmfval  29267  esum2d  29482  txprel  31156  relsset  31165  elfuns  31192  fnsingle  31196  funimage  31205  bj-elid  32262  mblfinlem1  32616  rngosn3  32893  dihvalrel  35586  relintabex  36906  cnvcnvintabd  36925  cnvintabd  36928  clcnvlem  36949  rfovcnvf1od  37318  relopabVD  38159