Definition df-br 3876

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 4743). (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 3875	. 2 wff 𝐴𝑅𝐵
5	1, 2	cop 3477	. . 3 class ⟨𝐴, 𝐵⟩
6	5, 3	wcel 1448	. 2 wff ⟨𝐴, 𝐵⟩ ∈ 𝑅
7	4, 6	wb 104	1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

This definition is referenced by:  breq  3877  breq1  3878  breq2  3879  ssbrd  3916  nfbrd  3918  brun  3921  brin  3922  brdif  3923  opabss  3932  brabsb  4121  brabga  4124  epelg  4150  pofun  4172  brxp  4508  brab2a  4530  brab2ga  4552  eqbrriv  4572  eqbrrdv  4574  eqbrrdiv  4575  opeliunxp2  4617  opelco2g  4645  opelco  4649  cnvss  4650  elcnv2  4655  opelcnvg  4657  brcnvg  4658  dfdm3  4664  dfrn3  4666  elrng  4668  eldm2g  4673  breldm  4681  dmopab  4688  opelrng  4709  opelrn  4711  elrn  4720  rnopab  4724  brres  4761  brresg  4763  resieq  4765  opelresi  4766  resiexg  4800  iss  4801  dfres2  4807  dfima3  4820  elima3  4824  imai  4831  elimasn  4842  eliniseg  4845  cotr  4856  issref  4857  cnvsym  4858  intasym  4859  asymref  4860  intirr  4861  codir  4863  qfto  4864  poirr2  4867  dmsnm  4940  coiun  4984  co02  4988  coi1  4990  dffun4  5070  dffun4f  5075  funeu2  5085  funopab  5094  funco  5099  funcnvsn  5104  isarep1  5145  fnop  5162  fneu2  5164  brprcneu  5346  dffv3g  5349  tz6.12  5381  nfvres  5386  0fv  5388  funopfv  5393  fnopfvb  5395  fvmptss2  5428  funfvbrb  5465  dff3im  5497  dff4im  5498  f1ompt  5503  idref  5590  foeqcnvco  5623  f1eqcocnv  5624  fliftel  5626  fliftel1  5627  fliftcnv  5628  f1oiso  5659  ovprc  5738  brabvv  5749  1st2ndbr  6012  xporderlem  6058  opeliunxp2f  6065  rbropapd  6069  ottposg  6082  dftpos3  6089  dftpos4  6090  tposoprab  6107  tfrlem7  6144  tfrexlem  6161  ercnv  6380  brdifun  6386  swoord1  6388  swoord2  6389  0er  6393  elecg  6397  iinerm  6431  brecop  6449  idssen  6601  xpcomco  6649  ltdfpr  7215  xrlenlt  7701  frecuzrdgtcl  10026  frecuzrdgfunlem  10033  climcau  10955  divides  11290  isstructim  11755  isstructr  11756  lmrcl  12142  lmff  12199  xmeterval  12363  eldvap  12524