Definition df-br 4131

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 5051). (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
df-br	⊢ (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

Detailed syntax breakdown of Definition df-br

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cR	. . 3 class 𝑅
4	1, 2, 3	wbr 4130	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3712	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2209	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 105	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is used by:  breq  4132  breq1  4133  breq2  4134  ssbrd  4173  nfbrd  4176  br0  4179  brne0  4180  brm  4181  brun  4182  brin  4183  brdif  4184  opabss  4195  brabsb  4403  brabga  4406  epelg  4435  pofun  4457  brxp  4805  brab2a  4828  brab2ga  4850  eqbrriv  4870  eqbrrdv  4872  eqbrrdiv  4873  opeliunxp2  4920  opelco2g  4948  opelco  4952  cnvss  4953  elcnv2  4958  opelcnvg  4960  brcnvg  4961  dfdm3  4967  dfrn3  4969  elrng  4971  eldm2g  4977  breldm  4985  dmopab  4992  opelrng  5014  opelrn  5016  elrn  5025  rnopab  5029  brres  5069  brresg  5071  resieq  5073  opelresi  5074  resiexg  5108  iss  5109  dfres2  5115  restidsing  5119  dfima3  5129  elima3  5133  imai  5143  elimasn  5154  eliniseg  5157  cotr  5169  issref  5170  cnvsym  5171  intasym  5172  asymref  5173  intirr  5174  codir  5176  qfto  5177  poirr2  5180  dmsnm  5253  coiun  5297  co02  5301  coi1  5303  dffun4  5388  dffun4f  5393  funeu2  5403  funopab  5412  funco  5417  funcnvsn  5426  isarep1  5467  fnop  5486  fneu2  5488  brprcneu  5688  dffv3g  5691  tz6.12  5723  nfvres  5732  0fv  5734  funopfv  5740  fnopfvb  5742  fvmptss2  5780  funfvbrb  5822  dff3im  5853  dff4im  5854  f1ompt  5859  idref  5962  foeqcnvco  5996  f1eqcocnv  5997  fliftel  5999  fliftel1  6000  fliftcnv  6001  f1oiso  6032  ovprc  6121  brabvv  6134  1st2ndbr  6418  xporderlem  6467  cnvimadfsn  6485  opeliunxp2f  6509  rbropapd  6513  ottposg  6526  dftpos3  6533  dftpos4  6534  tposoprab  6551  tfrlem7  6588  tfrexlem  6605  ercnv  6828  brdifun  6834  swoord1  6836  swoord2  6837  0er  6841  elecg  6847  iinerm  6881  brecop  6899  idssen  7063  xpcomco  7124  netap  7620  2omotaplemap  7623  exmidapne  7626  ltdfpr  7873  xrlenlt  8390  aprcl  8974  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  climcau  12113  divides  12556  isstructim  13366  isstructr  13367  imasaddfnlemg  13635  subrgdvds  14543  aprval  14591  lmrcl  15293  lmff  15350  xmeterval  15536  eldvap  15783  dvef  15828  iswlk  16564  wlkv  16567  wlkcprim  16591  wlklenvclwlk  16614  trlsv  16625  istrl  16626  eupthv  16687  iseupth  16688