ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-br GIF version

Definition df-br 3900
Description: Define a general binary relation. Note that the syntax is simply three class symbols in a row. Definition 6.18 of [TakeutiZaring] p. 29 generalized to arbitrary classes. This definition of relations is well-defined, although not very meaningful, when classes 𝐴 and/or 𝐵 are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when 𝑅 is a proper class (see for example iprc 4777). (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
df-br (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

Detailed syntax breakdown of Definition df-br
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cR . . 3 class 𝑅
41, 2, 3wbr 3899 . 2 wff 𝐴𝑅𝐵
51, 2cop 3500 . . 3 class 𝐴, 𝐵
65, 3wcel 1465 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 104 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff set class
This definition is referenced by:  breq  3901  breq1  3902  breq2  3903  ssbrd  3941  nfbrd  3943  br0  3946  brne0  3947  brm  3948  brun  3949  brin  3950  brdif  3951  opabss  3962  brabsb  4153  brabga  4156  epelg  4182  pofun  4204  brxp  4540  brab2a  4562  brab2ga  4584  eqbrriv  4604  eqbrrdv  4606  eqbrrdiv  4607  opeliunxp2  4649  opelco2g  4677  opelco  4681  cnvss  4682  elcnv2  4687  opelcnvg  4689  brcnvg  4690  dfdm3  4696  dfrn3  4698  elrng  4700  eldm2g  4705  breldm  4713  dmopab  4720  opelrng  4741  opelrn  4743  elrn  4752  rnopab  4756  brres  4795  brresg  4797  resieq  4799  opelresi  4800  resiexg  4834  iss  4835  dfres2  4841  dfima3  4854  elima3  4858  imai  4865  elimasn  4876  eliniseg  4879  cotr  4890  issref  4891  cnvsym  4892  intasym  4893  asymref  4894  intirr  4895  codir  4897  qfto  4898  poirr2  4901  dmsnm  4974  coiun  5018  co02  5022  coi1  5024  dffun4  5104  dffun4f  5109  funeu2  5119  funopab  5128  funco  5133  funcnvsn  5138  isarep1  5179  fnop  5196  fneu2  5198  brprcneu  5382  dffv3g  5385  tz6.12  5417  nfvres  5422  0fv  5424  funopfv  5429  fnopfvb  5431  fvmptss2  5464  funfvbrb  5501  dff3im  5533  dff4im  5534  f1ompt  5539  idref  5626  foeqcnvco  5659  f1eqcocnv  5660  fliftel  5662  fliftel1  5663  fliftcnv  5664  f1oiso  5695  ovprc  5774  brabvv  5785  1st2ndbr  6050  xporderlem  6096  opeliunxp2f  6103  rbropapd  6107  ottposg  6120  dftpos3  6127  dftpos4  6128  tposoprab  6145  tfrlem7  6182  tfrexlem  6199  ercnv  6418  brdifun  6424  swoord1  6426  swoord2  6427  0er  6431  elecg  6435  iinerm  6469  brecop  6487  idssen  6639  xpcomco  6688  ltdfpr  7282  xrlenlt  7797  aprcl  8375  frecuzrdgtcl  10140  frecuzrdgfunlem  10147  climcau  11071  divides  11407  isstructim  11884  isstructr  11885  lmrcl  12271  lmff  12329  xmeterval  12515  eldvap  12731  dvef  12767
  Copyright terms: Public domain W3C validator