Definition df-br 3729

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 A and/or B 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 4516). (Contributed by NM, 31-Dec-1993.)

Assertion

Ref	Expression
df-br	⊢ (A𝑅B ↔ ⟨A, B⟩ ∈ 𝑅)

Detailed syntax breakdown of Definition df-br

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cR	. . 3 class 𝑅
4	1, 2, 3	wbr 3728	. 2 wff A𝑅B
5	1, 2	cop 3343	. . 3 class ⟨A, B⟩
6	5, 3	wcel 1367	. 2 wff ⟨A, B⟩ ∈ 𝑅
7	4, 6	wb 98	1 wff (A𝑅B ↔ ⟨A, B⟩ ∈ 𝑅)

This definition is referenced by:  breq  3730  breq1  3731  breq2  3732  ssbrd  3769  nfbrd  3771  brun  3774  brin  3775  brdif  3776  opabss  3785  brabsb  3962  brabga  3965  epelg  3991  pofun  4013  brxp  4291  brab2a  4309  brab2ga  4331  eqbrriv  4351  eqbrrdv  4353  eqbrrdiv  4354  opeliunxp2  4392  opelco2g  4419  opelco  4423  cnvss  4424  elcnv2  4429  opelcnvg  4431  brcnvg  4432  dfdm3  4438  dfrn3  4440  elrng  4442  eldm2g  4447  breldm  4455  dmopab  4462  opelrng  4482  opelrn  4484  elrn  4493  rnopab  4497  brres  4534  brresg  4536  resieq  4538  opelresi  4539  resiexg  4569  iss  4570  dfres2  4574  dfima3  4587  elima3  4591  imai  4597  elimasn  4608  eliniseg  4611  cotr  4622  issref  4623  cnvsym  4624  intasym  4625  asymref  4626  intirr  4627  codir  4629  qfto  4630  poirr2  4633  dmsnm  4702  coiun  4746  co02  4750  coi1  4752  dffun4  4829  dffun4f  4833  funeu2  4842  funopab  4850  funco  4855  funcnvsn  4860  isarep1  4900  fnop  4917  fneu2  4919  brprcneu  5085  dffv3g  5088  tz6.12  5115  nfvres  5120  0fv  5122  funopfv  5127  fnopfvb  5129  fvmptss2  5161  funfvbrb  5194  dff3im  5226  dff4im  5227  f1ompt  5234  idref  5310  foeqcnvco  5344  f1eqcocnv  5345  fliftel  5347  fliftel1  5348  fliftcnv  5349  f1oiso  5379  ovprc  5452  brabvv  5463  1st2ndbr  5722  xporderlem  5763  isprmpt2  5769  ottposg  5781  dftpos3  5788  dftpos4  5789  tposoprab  5806  tfrlem7  5844  tfrexlem  5859  ercnv  6027  brdifun  6033  swoord1  6035  swoord2  6036  0er  6040  elecg  6044  iinerm  6078  brecop  6096  ltdfpr  6347  xrlenlt  6685