Definition df-br 4087

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

This definition is referenced by:  breq  4088  breq1  4089  breq2  4090  ssbrd  4129  nfbrd  4132  br0  4135  brne0  4136  brm  4137  brun  4138  brin  4139  brdif  4140  opabss  4151  brabsb  4353  brabga  4356  epelg  4385  pofun  4407  brxp  4754  brab2a  4777  brab2ga  4799  eqbrriv  4819  eqbrrdv  4821  eqbrrdiv  4822  opeliunxp2  4868  opelco2g  4896  opelco  4900  cnvss  4901  elcnv2  4906  opelcnvg  4908  brcnvg  4909  dfdm3  4915  dfrn3  4917  elrng  4919  eldm2g  4925  breldm  4933  dmopab  4940  opelrng  4962  opelrn  4964  elrn  4973  rnopab  4977  brres  5017  brresg  5019  resieq  5021  opelresi  5022  resiexg  5056  iss  5057  dfres2  5063  restidsing  5067  dfima3  5077  elima3  5081  imai  5090  elimasn  5101  eliniseg  5104  cotr  5116  issref  5117  cnvsym  5118  intasym  5119  asymref  5120  intirr  5121  codir  5123  qfto  5124  poirr2  5127  dmsnm  5200  coiun  5244  co02  5248  coi1  5250  dffun4  5335  dffun4f  5340  funeu2  5350  funopab  5359  funco  5364  funcnvsn  5372  isarep1  5413  fnop  5432  fneu2  5434  brprcneu  5628  dffv3g  5631  tz6.12  5663  nfvres  5671  0fv  5673  funopfv  5679  fnopfvb  5681  fvmptss2  5717  funfvbrb  5756  dff3im  5788  dff4im  5789  f1ompt  5794  idref  5892  foeqcnvco  5926  f1eqcocnv  5927  fliftel  5929  fliftel1  5930  fliftcnv  5931  f1oiso  5962  ovprc  6049  brabvv  6062  1st2ndbr  6342  xporderlem  6391  opeliunxp2f  6399  rbropapd  6403  ottposg  6416  dftpos3  6423  dftpos4  6424  tposoprab  6441  tfrlem7  6478  tfrexlem  6495  ercnv  6718  brdifun  6724  swoord1  6726  swoord2  6727  0er  6731  elecg  6737  iinerm  6771  brecop  6789  idssen  6945  xpcomco  7005  netap  7463  2omotaplemap  7466  exmidapne  7469  ltdfpr  7716  xrlenlt  8234  aprcl  8816  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  climcau  11898  divides  12340  isstructim  13086  isstructr  13087  imasaddfnlemg  13387  subrgdvds  14239  aprval  14286  lmrcl  14906  lmff  14963  xmeterval  15149  eldvap  15396  dvef  15441  iswlk  16120  wlkv  16123  wlkcprim  16147  wlklenvclwlk  16170  trlsv  16179  istrl  16180  eupthv  16241  iseupth  16242