Definition df-br 4115

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

This definition is referenced by:  breq  4116  breq1  4117  breq2  4118  ssbrd  4157  nfbrd  4160  br0  4163  brne0  4164  brm  4165  brun  4166  brin  4167  brdif  4168  opabss  4179  brabsb  4384  brabga  4387  epelg  4416  pofun  4438  brxp  4785  brab2a  4808  brab2ga  4830  eqbrriv  4850  eqbrrdv  4852  eqbrrdiv  4853  opeliunxp2  4900  opelco2g  4928  opelco  4932  cnvss  4933  elcnv2  4938  opelcnvg  4940  brcnvg  4941  dfdm3  4947  dfrn3  4949  elrng  4951  eldm2g  4957  breldm  4965  dmopab  4972  opelrng  4994  opelrn  4996  elrn  5005  rnopab  5009  brres  5049  brresg  5051  resieq  5053  opelresi  5054  resiexg  5088  iss  5089  dfres2  5095  restidsing  5099  dfima3  5109  elima3  5113  imai  5123  elimasn  5134  eliniseg  5137  cotr  5149  issref  5150  cnvsym  5151  intasym  5152  asymref  5153  intirr  5154  codir  5156  qfto  5157  poirr2  5160  dmsnm  5233  coiun  5277  co02  5281  coi1  5283  dffun4  5368  dffun4f  5373  funeu2  5383  funopab  5392  funco  5397  funcnvsn  5406  isarep1  5447  fnop  5466  fneu2  5468  brprcneu  5668  dffv3g  5671  tz6.12  5703  nfvres  5711  0fv  5713  funopfv  5719  fnopfvb  5721  fvmptss2  5757  funfvbrb  5796  dff3im  5827  dff4im  5828  f1ompt  5833  idref  5935  foeqcnvco  5969  f1eqcocnv  5970  fliftel  5972  fliftel1  5973  fliftcnv  5974  f1oiso  6005  ovprc  6094  brabvv  6107  1st2ndbr  6391  xporderlem  6440  cnvimadfsn  6458  opeliunxp2f  6482  rbropapd  6486  ottposg  6499  dftpos3  6506  dftpos4  6507  tposoprab  6524  tfrlem7  6561  tfrexlem  6578  ercnv  6801  brdifun  6807  swoord1  6809  swoord2  6810  0er  6814  elecg  6820  iinerm  6854  brecop  6872  idssen  7029  xpcomco  7090  netap  7584  2omotaplemap  7587  exmidapne  7590  ltdfpr  7837  xrlenlt  8354  aprcl  8937  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  climcau  12057  divides  12500  isstructim  13310  isstructr  13311  imasaddfnlemg  13578  subrgdvds  14481  aprval  14529  lmrcl  15183  lmff  15240  xmeterval  15426  eldvap  15673  dvef  15718  iswlk  16444  wlkv  16447  wlkcprim  16471  wlklenvclwlk  16494  trlsv  16505  istrl  16506  eupthv  16567  iseupth  16568