Definition df-br 3339

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 R normally denotes a relation such as "< " that compares two classes A and B, which might be numbers such as 1 and 2. This definition 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.

Assertion

Ref	Expression
df-br	|- (ARB <-> <.A, B>. e. R)

Detailed syntax breakdown of Definition df-br

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cR	. . 3 class R
4	1, 2, 3	wbr 3338	. 2 wff ARB
5	1, 2	cop 3046	. . 3 class <.A, B>.
6	5, 3	wcel 1300	. 2 wff <.A, B>. e. R
7	4, 6	wb 163	1 wff (ARB <-> <.A, B>. e. R)

This definition is referenced by:  breq 3340  breq1 3341  breq2 3342  ssbrd 3378  hbbr 3381  hbbrd 3382  brprc 3386  brun 3387  brin 3388  brdif 3389  opabss 3397  opabssOLD 3398  brabsb 3566  brabg 3568  posn 3603  brrelex 4028  brxp 4038  brelg 4047  brinxp2 4057  eqbrriv 4082  opelxpex2 4119  opelxpex2OLD 4120  opelco 4130  brco 4132  opelco2g 4133  cnvss 4134  elcnv2 4138  opelcnvg 4140  opelcnvgOLD 4141  brcnvg 4142  cnvcoOLD 4146  dfdm3 4148  dfrn3 4150  eldm2 4154  breldm 4161  opelrn 4192  elrn 4197  dmcossOLD 4212  brres 4223  resieq 4227  resiexg 4253  iss 4254  issOLD 4255  dfima2OLD 4266  dfima3 4267  dfima3OLD 4268  elima3 4272  imai 4280  elimasn 4289  elimasni 4292  eliniseg 4294  elinisegOLD 4295  cotr 4302  cotrOLD 4303  cnvsym 4304  cnvsymOLD 4305  intasym 4306  intasymOLD 4307  asymref 4308  asymrefOLD 4309  asymref2 4310  intirr 4312  intirrOLD 4313  cnviOLD 4321  rninxpOLD 4356  dmsnn0 4362  coiun 4407  co02 4411  coi1 4413  coass 4415  dffun4 4433  dffun5 4434  funeu2 4446  dffun8OLD 4449  funopab 4455  funsn 4463  funinOLD 4485  isarep1 4497  isarep1OLD 4498  fnop 4516  fneu2 4519  fcoi1OLD 4585  fcoi2OLD 4587  fv2 4676  tz6.12 4694  funopfv 4710  fnopfvb 4713  funopfvb 4715  fvelima 4723  dffv2 4734  fvopab5 4756  dff3 4790  dff4 4791  fvi 4818  f1oiso 4881  oprprc1 4908  fparlem1 5081  fparlem2 5082  fparlem3 5083  fparlem4 5084  dfec2 5321  brecop 5365  ecopoprdm 5368  brsdom 5440  brdom2 5447  idssen 5465  sbthcl 5522  brsdom2 5524  aceq3lem 5894  brdom3 5963  brdom7disj 5966  brdom6disj 5967  ltpiord 6167  ltxr 6664  xrlenlt 6670  eltopsp 8873  tpsex 8874  ismsg 9077  isgalem 9449  gapmlem 9461  isring 9465  avril1 10142  helloworld 10144  fora 10408  isdivrng 10417  divides 13664  dif2relOLD 13828  brtp 13830  fundmpss 13836  elrng 13878  elpredg 13889  xporderlem 13948  frxp 13951  wfrlem11 13967  brv 14063  symdif2rel 14064  brtxp 14067  brsset 14069  brbigcup 14074  eltids 14369  ref4w 14370  restidsing 14391  prj1 14395  inclrel 14444  deref 14633  vecval1b 14794  istopgrp 14971  mlteqer 15017  opncldf1 15402  compfipin0 15436  islocfin 15506  filnetlem4 15643  pofun 15772  eqbrrdv 16252  brabsb2 16253  eqbrrdv2 16255  cmtval 16938  cvrval 16988

Copyright terms: Public domain