MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-rel Structured version   Visualization version   GIF version

Definition df-rel 5034
Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5487 and dfrel3 5495. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
df-rel (Rel 𝐴𝐴 ⊆ (V × V))

Detailed syntax breakdown of Definition df-rel
StepHypRef Expression
1 cA . . 3 class 𝐴
21wrel 5032 . 2 wff Rel 𝐴
3 cvv 3172 . . . 4 class V
43, 3cxp 5025 . . 3 class (V × V)
51, 4wss 3539 . 2 wff 𝐴 ⊆ (V × V)
62, 5wb 194 1 wff (Rel 𝐴𝐴 ⊆ (V × V))
Colors of variables: wff setvar class
This definition is referenced by:  brrelex12  5068  releq  5113  nfrel  5116  sbcrel  5117  relss  5118  ssrel  5119  elrel  5133  relsn  5134  relxp  5138  relun  5146  reliun  5150  reliin  5151  rel0  5154  relopabi  5155  exopxfr2  5175  relop  5181  eqbrrdva  5200  elreldm  5257  issref  5414  cnvcnv  5490  relrelss  5561  cnviin  5574  nfunv  5820  dff3  6264  oprabss  6621  relmptopab  6758  1st2nd  7082  1stdm  7083  releldm2  7086  relmpt2opab  7123  reldmtpos  7224  dmtpos  7228  dftpos4  7235  tpostpos  7236  iiner  7683  fundmen  7893  nqerf  9608  uzrdgfni  12576  hashfun  13038  reltrclfv  13554  homarel  16457  relxpchom  16592  ustrel  21772  utop2nei  21811  utop3cls  21812  metustrel  22114  pi1xfrcnv  22612  reldv  23384  dvbsss  23416  uhgraopelvv  25619  vcex  26610  ssrelf  28598  1stpreimas  28659  fpwrelmap  28689  metideq  29057  metider  29058  pstmfval  29060  esum2d  29275  txprel  30949  relsset  30958  elfuns  30985  fnsingle  30989  funimage  30998  bj-elid  32045  mblfinlem1  32399  rngosn3  32676  dihvalrel  35369  relintabex  36689  cnvcnvintabd  36708  cnvintabd  36711  clcnvlem  36732  rfovcnvf1od  37101  relopabVD  37942
  Copyright terms: Public domain W3C validator