Definition df-br 4089

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 5001). (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 4088	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3672	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2202	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 105	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  4090  breq1  4091  breq2  4092  ssbrd  4131  nfbrd  4134  br0  4137  brne0  4138  brm  4139  brun  4140  brin  4141  brdif  4142  opabss  4153  brabsb  4355  brabga  4358  epelg  4387  pofun  4409  brxp  4756  brab2a  4779  brab2ga  4801  eqbrriv  4821  eqbrrdv  4823  eqbrrdiv  4824  opeliunxp2  4870  opelco2g  4898  opelco  4902  cnvss  4903  elcnv2  4908  opelcnvg  4910  brcnvg  4911  dfdm3  4917  dfrn3  4919  elrng  4921  eldm2g  4927  breldm  4935  dmopab  4942  opelrng  4964  opelrn  4966  elrn  4975  rnopab  4979  brres  5019  brresg  5021  resieq  5023  opelresi  5024  resiexg  5058  iss  5059  dfres2  5065  restidsing  5069  dfima3  5079  elima3  5083  imai  5092  elimasn  5103  eliniseg  5106  cotr  5118  issref  5119  cnvsym  5120  intasym  5121  asymref  5122  intirr  5123  codir  5125  qfto  5126  poirr2  5129  dmsnm  5202  coiun  5246  co02  5250  coi1  5252  dffun4  5337  dffun4f  5342  funeu2  5352  funopab  5361  funco  5366  funcnvsn  5375  isarep1  5416  fnop  5435  fneu2  5437  brprcneu  5632  dffv3g  5635  tz6.12  5667  nfvres  5675  0fv  5677  funopfv  5683  fnopfvb  5685  fvmptss2  5721  funfvbrb  5760  dff3im  5792  dff4im  5793  f1ompt  5798  idref  5897  foeqcnvco  5931  f1eqcocnv  5932  fliftel  5934  fliftel1  5935  fliftcnv  5936  f1oiso  5967  ovprc  6054  brabvv  6067  1st2ndbr  6347  xporderlem  6396  opeliunxp2f  6404  rbropapd  6408  ottposg  6421  dftpos3  6428  dftpos4  6429  tposoprab  6446  tfrlem7  6483  tfrexlem  6500  ercnv  6723  brdifun  6729  swoord1  6731  swoord2  6732  0er  6736  elecg  6742  iinerm  6776  brecop  6794  idssen  6950  xpcomco  7010  netap  7473  2omotaplemap  7476  exmidapne  7479  ltdfpr  7726  xrlenlt  8244  aprcl  8826  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  climcau  11925  divides  12368  isstructim  13114  isstructr  13115  imasaddfnlemg  13415  subrgdvds  14268  aprval  14315  lmrcl  14935  lmff  14992  xmeterval  15178  eldvap  15425  dvef  15470  iswlk  16193  wlkv  16196  wlkcprim  16220  wlklenvclwlk  16243  trlsv  16254  istrl  16255  eupthv  16316  iseupth  16317