Definition df-br 4129

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 5049). (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 4128	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3711	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2209	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 105	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  4130  breq1  4131  breq2  4132  ssbrd  4171  nfbrd  4174  br0  4177  brne0  4178  brm  4179  brun  4180  brin  4181  brdif  4182  opabss  4193  brabsb  4401  brabga  4404  epelg  4433  pofun  4455  brxp  4803  brab2a  4826  brab2ga  4848  eqbrriv  4868  eqbrrdv  4870  eqbrrdiv  4871  opeliunxp2  4918  opelco2g  4946  opelco  4950  cnvss  4951  elcnv2  4956  opelcnvg  4958  brcnvg  4959  dfdm3  4965  dfrn3  4967  elrng  4969  eldm2g  4975  breldm  4983  dmopab  4990  opelrng  5012  opelrn  5014  elrn  5023  rnopab  5027  brres  5067  brresg  5069  resieq  5071  opelresi  5072  resiexg  5106  iss  5107  dfres2  5113  restidsing  5117  dfima3  5127  elima3  5131  imai  5141  elimasn  5152  eliniseg  5155  cotr  5167  issref  5168  cnvsym  5169  intasym  5170  asymref  5171  intirr  5172  codir  5174  qfto  5175  poirr2  5178  dmsnm  5251  coiun  5295  co02  5299  coi1  5301  dffun4  5386  dffun4f  5391  funeu2  5401  funopab  5410  funco  5415  funcnvsn  5424  isarep1  5465  fnop  5484  fneu2  5486  brprcneu  5686  dffv3g  5689  tz6.12  5721  nfvres  5729  0fv  5731  funopfv  5737  fnopfvb  5739  fvmptss2  5777  funfvbrb  5816  dff3im  5847  dff4im  5848  f1ompt  5853  idref  5955  foeqcnvco  5989  f1eqcocnv  5990  fliftel  5992  fliftel1  5993  fliftcnv  5994  f1oiso  6025  ovprc  6114  brabvv  6127  1st2ndbr  6411  xporderlem  6460  cnvimadfsn  6478  opeliunxp2f  6502  rbropapd  6506  ottposg  6519  dftpos3  6526  dftpos4  6527  tposoprab  6544  tfrlem7  6581  tfrexlem  6598  ercnv  6821  brdifun  6827  swoord1  6829  swoord2  6830  0er  6834  elecg  6840  iinerm  6874  brecop  6892  idssen  7056  xpcomco  7117  netap  7613  2omotaplemap  7616  exmidapne  7619  ltdfpr  7866  xrlenlt  8383  aprcl  8967  frecuzrdgtcl  10830  frecuzrdgfunlem  10837  climcau  12094  divides  12537  isstructim  13347  isstructr  13348  imasaddfnlemg  13615  subrgdvds  14519  aprval  14567  lmrcl  15219  lmff  15276  xmeterval  15462  eldvap  15709  dvef  15754  iswlk  16481  wlkv  16484  wlkcprim  16508  wlklenvclwlk  16531  trlsv  16542  istrl  16543  eupthv  16604  iseupth  16605