Definition df-br 4060

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 4966). (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 4059	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3646	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 2178	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 105	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  4061  breq1  4062  breq2  4063  ssbrd  4102  nfbrd  4105  br0  4108  brne0  4109  brm  4110  brun  4111  brin  4112  brdif  4113  opabss  4124  brabsb  4325  brabga  4328  epelg  4355  pofun  4377  brxp  4724  brab2a  4746  brab2ga  4768  eqbrriv  4788  eqbrrdv  4790  eqbrrdiv  4791  opeliunxp2  4836  opelco2g  4864  opelco  4868  cnvss  4869  elcnv2  4874  opelcnvg  4876  brcnvg  4877  dfdm3  4883  dfrn3  4885  elrng  4887  eldm2g  4893  breldm  4901  dmopab  4908  opelrng  4929  opelrn  4931  elrn  4940  rnopab  4944  brres  4984  brresg  4986  resieq  4988  opelresi  4989  resiexg  5023  iss  5024  dfres2  5030  restidsing  5034  dfima3  5044  elima3  5048  imai  5057  elimasn  5068  eliniseg  5071  cotr  5083  issref  5084  cnvsym  5085  intasym  5086  asymref  5087  intirr  5088  codir  5090  qfto  5091  poirr2  5094  dmsnm  5167  coiun  5211  co02  5215  coi1  5217  dffun4  5301  dffun4f  5306  funeu2  5316  funopab  5325  funco  5330  funcnvsn  5338  isarep1  5379  fnop  5398  fneu2  5400  brprcneu  5592  dffv3g  5595  tz6.12  5627  nfvres  5633  0fv  5635  funopfv  5641  fnopfvb  5643  fvmptss2  5677  funfvbrb  5716  dff3im  5748  dff4im  5749  f1ompt  5754  idref  5848  foeqcnvco  5882  f1eqcocnv  5883  fliftel  5885  fliftel1  5886  fliftcnv  5887  f1oiso  5918  ovprc  6003  brabvv  6014  1st2ndbr  6293  xporderlem  6340  opeliunxp2f  6347  rbropapd  6351  ottposg  6364  dftpos3  6371  dftpos4  6372  tposoprab  6389  tfrlem7  6426  tfrexlem  6443  ercnv  6664  brdifun  6670  swoord1  6672  swoord2  6673  0er  6677  elecg  6683  iinerm  6717  brecop  6735  idssen  6891  xpcomco  6946  netap  7401  2omotaplemap  7404  exmidapne  7407  ltdfpr  7654  xrlenlt  8172  aprcl  8754  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  climcau  11773  divides  12215  isstructim  12961  isstructr  12962  imasaddfnlemg  13261  subrgdvds  14112  aprval  14159  lmrcl  14778  lmff  14836  xmeterval  15022  eldvap  15269  dvef  15314