Definition df-br 3990

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 4879). (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 3989	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3586	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2141	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 104	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  3991  breq1  3992  breq2  3993  ssbrd  4032  nfbrd  4034  br0  4037  brne0  4038  brm  4039  brun  4040  brin  4041  brdif  4042  opabss  4053  brabsb  4246  brabga  4249  epelg  4275  pofun  4297  brxp  4642  brab2a  4664  brab2ga  4686  eqbrriv  4706  eqbrrdv  4708  eqbrrdiv  4709  opeliunxp2  4751  opelco2g  4779  opelco  4783  cnvss  4784  elcnv2  4789  opelcnvg  4791  brcnvg  4792  dfdm3  4798  dfrn3  4800  elrng  4802  eldm2g  4807  breldm  4815  dmopab  4822  opelrng  4843  opelrn  4845  elrn  4854  rnopab  4858  brres  4897  brresg  4899  resieq  4901  opelresi  4902  resiexg  4936  iss  4937  dfres2  4943  dfima3  4956  elima3  4960  imai  4967  elimasn  4978  eliniseg  4981  cotr  4992  issref  4993  cnvsym  4994  intasym  4995  asymref  4996  intirr  4997  codir  4999  qfto  5000  poirr2  5003  dmsnm  5076  coiun  5120  co02  5124  coi1  5126  dffun4  5209  dffun4f  5214  funeu2  5224  funopab  5233  funco  5238  funcnvsn  5243  isarep1  5284  fnop  5301  fneu2  5303  brprcneu  5489  dffv3g  5492  tz6.12  5524  nfvres  5529  0fv  5531  funopfv  5536  fnopfvb  5538  fvmptss2  5571  funfvbrb  5609  dff3im  5641  dff4im  5642  f1ompt  5647  idref  5736  foeqcnvco  5769  f1eqcocnv  5770  fliftel  5772  fliftel1  5773  fliftcnv  5774  f1oiso  5805  ovprc  5888  brabvv  5899  1st2ndbr  6163  xporderlem  6210  opeliunxp2f  6217  rbropapd  6221  ottposg  6234  dftpos3  6241  dftpos4  6242  tposoprab  6259  tfrlem7  6296  tfrexlem  6313  ercnv  6534  brdifun  6540  swoord1  6542  swoord2  6543  0er  6547  elecg  6551  iinerm  6585  brecop  6603  idssen  6755  xpcomco  6804  ltdfpr  7468  xrlenlt  7984  aprcl  8565  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  climcau  11310  divides  11751  isstructim  12430  isstructr  12431  lmrcl  12985  lmff  13043  xmeterval  13229  eldvap  13445  dvef  13482