Definition df-br 4112

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 5028). (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 4111	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3694	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2205	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 105	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  4113  breq1  4114  breq2  4115  ssbrd  4154  nfbrd  4157  br0  4160  brne0  4161  brm  4162  brun  4163  brin  4164  brdif  4165  opabss  4176  brabsb  4381  brabga  4384  epelg  4413  pofun  4435  brxp  4782  brab2a  4805  brab2ga  4827  eqbrriv  4847  eqbrrdv  4849  eqbrrdiv  4850  opeliunxp2  4897  opelco2g  4925  opelco  4929  cnvss  4930  elcnv2  4935  opelcnvg  4937  brcnvg  4938  dfdm3  4944  dfrn3  4946  elrng  4948  eldm2g  4954  breldm  4962  dmopab  4969  opelrng  4991  opelrn  4993  elrn  5002  rnopab  5006  brres  5046  brresg  5048  resieq  5050  opelresi  5051  resiexg  5085  iss  5086  dfres2  5092  restidsing  5096  dfima3  5106  elima3  5110  imai  5120  elimasn  5131  eliniseg  5134  cotr  5146  issref  5147  cnvsym  5148  intasym  5149  asymref  5150  intirr  5151  codir  5153  qfto  5154  poirr2  5157  dmsnm  5230  coiun  5274  co02  5278  coi1  5280  dffun4  5365  dffun4f  5370  funeu2  5380  funopab  5389  funco  5394  funcnvsn  5403  isarep1  5444  fnop  5463  fneu2  5465  brprcneu  5665  dffv3g  5668  tz6.12  5700  nfvres  5708  0fv  5710  funopfv  5716  fnopfvb  5718  fvmptss2  5754  funfvbrb  5793  dff3im  5824  dff4im  5825  f1ompt  5830  idref  5931  foeqcnvco  5965  f1eqcocnv  5966  fliftel  5968  fliftel1  5969  fliftcnv  5970  f1oiso  6001  ovprc  6088  brabvv  6101  1st2ndbr  6380  xporderlem  6429  cnvimadfsn  6447  opeliunxp2f  6471  rbropapd  6475  ottposg  6488  dftpos3  6495  dftpos4  6496  tposoprab  6513  tfrlem7  6550  tfrexlem  6567  ercnv  6790  brdifun  6796  swoord1  6798  swoord2  6799  0er  6803  elecg  6809  iinerm  6843  brecop  6861  idssen  7018  xpcomco  7079  netap  7570  2omotaplemap  7573  exmidapne  7576  ltdfpr  7823  xrlenlt  8340  aprcl  8922  frecuzrdgtcl  10778  frecuzrdgfunlem  10785  climcau  12036  divides  12479  isstructim  13243  isstructr  13244  imasaddfnlemg  13544  subrgdvds  14397  aprval  14445  lmrcl  15074  lmff  15131  xmeterval  15317  eldvap  15564  dvef  15609  iswlk  16335  wlkv  16338  wlkcprim  16362  wlklenvclwlk  16385  trlsv  16396  istrl  16397  eupthv  16458  iseupth  16459