Definition df-br 4132

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

This definition is used by:  breq  4133  breq1  4134  breq2  4135  ssbrd  4174  nfbrd  4177  br0  4180  brne0  4181  brm  4182  brun  4183  brin  4184  brdif  4185  opabss  4196  brabsb  4405  brabga  4408  epelg  4437  pofun  4459  brxp  4807  brab2a  4830  brab2ga  4852  eqbrriv  4872  eqbrrdv  4874  eqbrrdiv  4875  opeliunxp2  4922  opelco2g  4950  opelco  4954  cnvss  4955  elcnv2  4960  opelcnvg  4962  brcnvg  4963  dfdm3  4969  dfrn3  4971  elrng  4973  eldm2g  4979  breldm  4987  dmopab  4994  opelrng  5016  opelrn  5018  elrn  5027  rnopab  5031  brres  5071  brresg  5073  resieq  5075  opelresi  5076  resiexg  5111  iss  5112  dfres2  5118  restidsing  5122  dfima3  5132  elima3  5136  imai  5146  elimasn  5157  eliniseg  5160  cotr  5172  issref  5173  cnvsym  5174  intasym  5175  asymref  5176  intirr  5177  codir  5179  qfto  5180  poirr2  5183  dmsnm  5256  coiun  5300  co02  5304  coi1  5306  dffun4  5391  dffun4f  5396  funeu2  5406  funopab  5415  funco  5420  funcnvsn  5429  isarep1  5470  fnop  5489  fneu2  5491  brprcneu  5691  dffv3g  5694  tz6.12  5726  nfvres  5735  0fv  5737  funopfv  5743  fnopfvb  5745  fvmptss2  5783  funfvbrb  5825  dff3im  5856  dff4im  5857  f1ompt  5862  idref  5965  foeqcnvco  5999  f1eqcocnv  6000  fliftel  6002  fliftel1  6003  fliftcnv  6004  f1oiso  6035  ovprc  6124  brabvv  6137  1st2ndbr  6422  xporderlem  6471  cnvimadfsn  6489  opeliunxp2f  6513  rbropapd  6517  ottposg  6530  dftpos3  6537  dftpos4  6538  tposoprab  6555  tfrlem7  6592  tfrexlem  6609  ercnv  6832  brdifun  6838  swoord1  6840  swoord2  6841  0er  6845  elecg  6851  iinerm  6885  brecop  6903  idssen  7067  xpcomco  7128  netap  7626  2omotaplemap  7629  exmidapne  7632  ltdfpr  7879  xrlenlt  8396  aprcl  8982  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  climcau  12138  divides  12581  isstructim  13424  isstructr  13425  imasaddfnlemg  13694  subrgdvds  14652  aprval  14700  lmrcl  15418  lmff  15475  xmeterval  15661  eldvap  15908  dvef  15953  iswlk  16769  wlkv  16772  wlkcprim  16796  wlklenvclwlk  16819  trlsv  16830  istrl  16831  eupthv  16892  iseupth  16893