Definition df-br 4084

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 4996). (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 4083	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3669	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2200	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 105	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  4085  breq1  4086  breq2  4087  ssbrd  4126  nfbrd  4129  br0  4132  brne0  4133  brm  4134  brun  4135  brin  4136  brdif  4137  opabss  4148  brabsb  4350  brabga  4353  epelg  4382  pofun  4404  brxp  4751  brab2a  4774  brab2ga  4796  eqbrriv  4816  eqbrrdv  4818  eqbrrdiv  4819  opeliunxp2  4865  opelco2g  4893  opelco  4897  cnvss  4898  elcnv2  4903  opelcnvg  4905  brcnvg  4906  dfdm3  4912  dfrn3  4914  elrng  4916  eldm2g  4922  breldm  4930  dmopab  4937  opelrng  4959  opelrn  4961  elrn  4970  rnopab  4974  brres  5014  brresg  5016  resieq  5018  opelresi  5019  resiexg  5053  iss  5054  dfres2  5060  restidsing  5064  dfima3  5074  elima3  5078  imai  5087  elimasn  5098  eliniseg  5101  cotr  5113  issref  5114  cnvsym  5115  intasym  5116  asymref  5117  intirr  5118  codir  5120  qfto  5121  poirr2  5124  dmsnm  5197  coiun  5241  co02  5245  coi1  5247  dffun4  5332  dffun4f  5337  funeu2  5347  funopab  5356  funco  5361  funcnvsn  5369  isarep1  5410  fnop  5429  fneu2  5431  brprcneu  5625  dffv3g  5628  tz6.12  5660  nfvres  5668  0fv  5670  funopfv  5676  fnopfvb  5678  fvmptss2  5714  funfvbrb  5753  dff3im  5785  dff4im  5786  f1ompt  5791  idref  5889  foeqcnvco  5923  f1eqcocnv  5924  fliftel  5926  fliftel1  5927  fliftcnv  5928  f1oiso  5959  ovprc  6046  brabvv  6059  1st2ndbr  6339  xporderlem  6388  opeliunxp2f  6395  rbropapd  6399  ottposg  6412  dftpos3  6419  dftpos4  6420  tposoprab  6437  tfrlem7  6474  tfrexlem  6491  ercnv  6714  brdifun  6720  swoord1  6722  swoord2  6723  0er  6727  elecg  6733  iinerm  6767  brecop  6785  idssen  6941  xpcomco  6998  netap  7456  2omotaplemap  7459  exmidapne  7462  ltdfpr  7709  xrlenlt  8227  aprcl  8809  frecuzrdgtcl  10651  frecuzrdgfunlem  10658  climcau  11879  divides  12321  isstructim  13067  isstructr  13068  imasaddfnlemg  13368  subrgdvds  14220  aprval  14267  lmrcl  14887  lmff  14944  xmeterval  15130  eldvap  15377  dvef  15422  iswlk  16095  wlkv  16098  wlkcprim  16122  wlklenvclwlk  16145  trlsv  16154  istrl  16155