New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-br Unicode version

Definition df-br 4640
 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. Class normally denotes a relation that compares two classes and . This definition 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. (Contributed by NM, 4-Jun-1995.)
Assertion
Ref Expression
df-br

Detailed syntax breakdown of Definition df-br
StepHypRef Expression
1 cA . . 3
2 cB . . 3
3 cR . . 3
41, 2, 3wbr 4639 . 2
51, 2cop 4561 . . 3
65, 3wcel 1710 . 2
74, 6wb 176 1
 Colors of variables: wff setvar class This definition is referenced by:  breq  4641  breq1  4642  breq2  4643  ssbrd  4680  nfbrd  4682  brex  4689  brun  4692  brin  4693  brdif  4694  opelopabsb  4697  brabsb  4698  brabga  4701  br1stg  4730  dfima2  4745  dfco1  4748  dfsi2  4751  elima3  4756  opelssetsn  4760  brxp  4812  eqbrriv  4851  opelco  4884  cnvss  4885  elcnv2  4890  opelcnv  4893  elrn2  4897  eldm2  4899  dfrn3  4903  breldm  4911  dmun  4912  dmopab  4915  elimapw1  4944  opelres  4950  dfima4  4952  opelrn  4961  rnopab  4967  iss  5000  dfres2  5002  imai  5010  elimasn  5019  eliniseg  5020  cotr  5026  cnvsym  5027  intasym  5028  intirr  5029  dmsnopg  5066  rnsnop  5075  dfco2  5080  coiun  5090  co02  5092  co01  5093  dffun2  5119  dffun4  5121  dffun5  5122  funeu2  5132  funopab  5139  funsn  5147  fnop  5186  fneu2  5188  fcnvres  5243  tz6.12  5345  funopfv  5357  fnopfvb  5359  funopfvb  5361  funfvbrb  5401  fvi  5442  f1oiso  5499  opsnelsi  5774  oteltxp  5782  brimage  5793  otsnelsi3  5805  composeex  5820  addcfnex  5824  funsex  5828  fnsex  5832  dmpprod  5840  crossex  5850  pw1fnex  5852  fnfullfunlem1  5856  fvfullfunlem2  5862  domfnex  5870  ranfnex  5871  clos1ex  5876  transex  5910  refex  5911  antisymex  5912  connexex  5913  foundex  5914  extex  5915  symex  5916  elec  5964  qsexg  5982  mapexi  6003  enex  6031  idssen  6040  enpw1lem1  6061  enmap2lem1  6063  enmap1lem1  6069  enprmaplem1  6076  nenpw1pwlem1  6084  ovmuc  6130  mucex  6133  ovcelem1  6171  ceex  6174  leconnnc  6218  tcfnex  6244  nmembers1lem1  6268  nncdiv3lem1  6275  nncdiv3lem2  6276  nnc3n3p1  6278  nchoicelem3  6291  nchoicelem10  6298  nchoicelem11  6299  nchoicelem16  6304  nchoicelem18  6306  fnfreclem1  6317  fnfreclem2  6318  fnfreclem3  6319  frecsuc  6322
 Copyright terms: Public domain W3C validator