Definition df-br 2063

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. Class R normally denotes a relation such as "<" that compares two classes A and B, which might be numbers such as 1 and 2. This definition 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 R is a proper class.

Assertion

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

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 R
4	1, 2, 3	wbr 2054	. 2 wff ARB
5	1, 2	cop 1810	. . 3 class ⟨A, B⟩
6	5, 3	wcel 1092	. 2 wff ⟨A, B⟩ ∈ R
7	4, 6	wb 127	1 wff (ARB ↔ ⟨A, B⟩ ∈ R)

This definition is referenced by:  breq 2064  breq1 2065  breq2 2066  ssbrd 2094  hbbr 2095  brprc 2097  opabss 2100  brabg 2116  brrelex 2446  brxp 2453  brelg 2458  brinxp 2466  brco 2510  opelcog 2511  cnvss 2512  elcnv2 2515  opelcnvg 2517  brcnv 2519  cnvco 2520  dfdm3 2522  dfrn3 2524  eldm2 2528  breldm 2535  opelrn 2560  elrn2 2563  dmco 2570  resieq 2581  iss 2599  dfima2 2604  dfima3 2605  elima3 2608  imai 2613  eliniseg 2618  cotr 2625  cnvsym 2626  intasym 2627  intirr 2628  cnvi 2634  cores 2659  co02 2663  coi1 2665  coass 2667  dmco2 2673  dffun4 2676  dffun5 2677  funeu2 2686  dffun7 2688  funopab 2694  funin 2708  fnop 2727  fneu2 2729  fcoi1 2765  fcoi2 2766  tz6.12 2843  funfvopi 2853  fnfvop 2856  fvelima 2859  fvi 2900  f1oiso 2942  oprprc1 3019  ec2 3203  brecop 3242  ecopoprdm 3245  brsdom 3286  brdom2 3292  idssen 3309  sbthcl 3361  brsdom2 3363  aceq3lem 3555  ltpiord 3809  leltt 4278  avril1 4523

metamath.org