Definition df-br 4094

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 5007). (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 4093	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3676	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2202	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 105	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  4095  breq1  4096  breq2  4097  ssbrd  4136  nfbrd  4139  br0  4142  brne0  4143  brm  4144  brun  4145  brin  4146  brdif  4147  opabss  4158  brabsb  4361  brabga  4364  epelg  4393  pofun  4415  brxp  4762  brab2a  4785  brab2ga  4807  eqbrriv  4827  eqbrrdv  4829  eqbrrdiv  4830  opeliunxp2  4876  opelco2g  4904  opelco  4908  cnvss  4909  elcnv2  4914  opelcnvg  4916  brcnvg  4917  dfdm3  4923  dfrn3  4925  elrng  4927  eldm2g  4933  breldm  4941  dmopab  4948  opelrng  4970  opelrn  4972  elrn  4981  rnopab  4985  brres  5025  brresg  5027  resieq  5029  opelresi  5030  resiexg  5064  iss  5065  dfres2  5071  restidsing  5075  dfima3  5085  elima3  5089  imai  5099  elimasn  5110  eliniseg  5113  cotr  5125  issref  5126  cnvsym  5127  intasym  5128  asymref  5129  intirr  5130  codir  5132  qfto  5133  poirr2  5136  dmsnm  5209  coiun  5253  co02  5257  coi1  5259  dffun4  5344  dffun4f  5349  funeu2  5359  funopab  5368  funco  5373  funcnvsn  5382  isarep1  5423  fnop  5442  fneu2  5444  brprcneu  5641  dffv3g  5644  tz6.12  5676  nfvres  5684  0fv  5686  funopfv  5692  fnopfvb  5694  fvmptss2  5730  funfvbrb  5769  dff3im  5800  dff4im  5801  f1ompt  5806  idref  5907  foeqcnvco  5941  f1eqcocnv  5942  fliftel  5944  fliftel1  5945  fliftcnv  5946  f1oiso  5977  ovprc  6064  brabvv  6077  1st2ndbr  6356  xporderlem  6405  cnvimadfsn  6423  opeliunxp2f  6447  rbropapd  6451  ottposg  6464  dftpos3  6471  dftpos4  6472  tposoprab  6489  tfrlem7  6526  tfrexlem  6543  ercnv  6766  brdifun  6772  swoord1  6774  swoord2  6775  0er  6779  elecg  6785  iinerm  6819  brecop  6837  idssen  6993  xpcomco  7053  netap  7533  2omotaplemap  7536  exmidapne  7539  ltdfpr  7786  xrlenlt  8303  aprcl  8885  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  climcau  11987  divides  12430  isstructim  13176  isstructr  13177  imasaddfnlemg  13477  subrgdvds  14330  aprval  14378  lmrcl  15003  lmff  15060  xmeterval  15246  eldvap  15493  dvef  15538  iswlk  16264  wlkv  16267  wlkcprim  16291  wlklenvclwlk  16314  trlsv  16325  istrl  16326  eupthv  16387  iseupth  16388