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

Definition df-br 3898
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  A and/or  B are proper classes (i.e. are not sets). On the other hand, we often find uses for this definition when  R is a proper class (see for example iprc 4775). (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
df-br  |-  ( A R B  <->  <. A ,  B >.  e.  R )

Detailed syntax breakdown of Definition df-br
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
3 cR . . 3  class  R
41, 2, 3wbr 3897 . 2  wff  A R B
51, 2cop 3498 . . 3  class  <. A ,  B >.
65, 3wcel 1463 . 2  wff  <. A ,  B >.  e.  R
74, 6wb 104 1  wff  ( A R B  <->  <. A ,  B >.  e.  R )
Colors of variables: wff set class
This definition is referenced by:  breq  3899  breq1  3900  breq2  3901  ssbrd  3939  nfbrd  3941  br0  3944  brne0  3945  brm  3946  brun  3947  brin  3948  brdif  3949  opabss  3960  brabsb  4151  brabga  4154  epelg  4180  pofun  4202  brxp  4538  brab2a  4560  brab2ga  4582  eqbrriv  4602  eqbrrdv  4604  eqbrrdiv  4605  opeliunxp2  4647  opelco2g  4675  opelco  4679  cnvss  4680  elcnv2  4685  opelcnvg  4687  brcnvg  4688  dfdm3  4694  dfrn3  4696  elrng  4698  eldm2g  4703  breldm  4711  dmopab  4718  opelrng  4739  opelrn  4741  elrn  4750  rnopab  4754  brres  4793  brresg  4795  resieq  4797  opelresi  4798  resiexg  4832  iss  4833  dfres2  4839  dfima3  4852  elima3  4856  imai  4863  elimasn  4874  eliniseg  4877  cotr  4888  issref  4889  cnvsym  4890  intasym  4891  asymref  4892  intirr  4893  codir  4895  qfto  4896  poirr2  4899  dmsnm  4972  coiun  5016  co02  5020  coi1  5022  dffun4  5102  dffun4f  5107  funeu2  5117  funopab  5126  funco  5131  funcnvsn  5136  isarep1  5177  fnop  5194  fneu2  5196  brprcneu  5380  dffv3g  5383  tz6.12  5415  nfvres  5420  0fv  5422  funopfv  5427  fnopfvb  5429  fvmptss2  5462  funfvbrb  5499  dff3im  5531  dff4im  5532  f1ompt  5537  idref  5624  foeqcnvco  5657  f1eqcocnv  5658  fliftel  5660  fliftel1  5661  fliftcnv  5662  f1oiso  5693  ovprc  5772  brabvv  5783  1st2ndbr  6048  xporderlem  6094  opeliunxp2f  6101  rbropapd  6105  ottposg  6118  dftpos3  6125  dftpos4  6126  tposoprab  6143  tfrlem7  6180  tfrexlem  6197  ercnv  6416  brdifun  6422  swoord1  6424  swoord2  6425  0er  6429  elecg  6433  iinerm  6467  brecop  6485  idssen  6637  xpcomco  6686  ltdfpr  7278  xrlenlt  7793  aprcl  8371  frecuzrdgtcl  10136  frecuzrdgfunlem  10143  climcau  11067  divides  11402  isstructim  11879  isstructr  11880  lmrcl  12266  lmff  12324  xmeterval  12510  eldvap  12726  dvef  12762
  Copyright terms: Public domain W3C validator