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  5896  foeqcnvco  5930  f1eqcocnv  5931  fliftel  5933  fliftel1  5934  fliftcnv  5935  f1oiso  5966  ovprc  6053  brabvv  6066  1st2ndbr  6346  xporderlem  6395  opeliunxp2f  6403  rbropapd  6407  ottposg  6420  dftpos3  6427  dftpos4  6428  tposoprab  6445  tfrlem7  6482  tfrexlem  6499  ercnv  6722  brdifun  6728  swoord1  6730  swoord2  6731  0er  6735  elecg  6741  iinerm  6775  brecop  6793  idssen  6949  xpcomco  7009  netap  7472  2omotaplemap  7475  exmidapne  7478  ltdfpr  7725  xrlenlt  8243  aprcl  8825  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  climcau  11907  divides  12349  isstructim  13095  isstructr  13096  imasaddfnlemg  13396  subrgdvds  14248  aprval  14295  lmrcl  14915  lmff  14972  xmeterval  15158  eldvap  15405  dvef  15450  iswlk  16173  wlkv  16176  wlkcprim  16200  wlklenvclwlk  16223  trlsv  16234  istrl  16235  eupthv  16296  iseupth  16297