ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-br GIF version

Definition df-br 3794
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 4628). (Contributed by NM, 31-Dec-1993.)
Assertion
Ref Expression
df-br (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)

Detailed syntax breakdown of Definition df-br
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cR . . 3 class 𝑅
41, 2, 3wbr 3793 . 2 wff 𝐴𝑅𝐵
51, 2cop 3409 . . 3 class 𝐴, 𝐵
65, 3wcel 1434 . 2 wff 𝐴, 𝐵⟩ ∈ 𝑅
74, 6wb 103 1 wff (𝐴𝑅𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ 𝑅)
Colors of variables: wff set class
This definition is referenced by:  breq  3795  breq1  3796  breq2  3797  ssbrd  3834  nfbrd  3836  brun  3839  brin  3840  brdif  3841  opabss  3850  brabsb  4024  brabga  4027  epelg  4053  pofun  4075  brxp  4401  brab2a  4419  brab2ga  4441  eqbrriv  4461  eqbrrdv  4463  eqbrrdiv  4464  opeliunxp2  4504  opelco2g  4531  opelco  4535  cnvss  4536  elcnv2  4541  opelcnvg  4543  brcnvg  4544  dfdm3  4550  dfrn3  4552  elrng  4554  eldm2g  4559  breldm  4567  dmopab  4574  opelrng  4594  opelrn  4596  elrn  4605  rnopab  4609  brres  4646  brresg  4648  resieq  4650  opelresi  4651  resiexg  4683  iss  4684  dfres2  4688  dfima3  4701  elima3  4705  imai  4711  elimasn  4722  eliniseg  4725  cotr  4736  issref  4737  cnvsym  4738  intasym  4739  asymref  4740  intirr  4741  codir  4743  qfto  4744  poirr2  4747  dmsnm  4816  coiun  4860  co02  4864  coi1  4866  dffun4  4943  dffun4f  4948  funeu2  4957  funopab  4965  funco  4970  funcnvsn  4975  isarep1  5016  fnop  5033  fneu2  5035  brprcneu  5202  dffv3g  5205  tz6.12  5233  nfvres  5238  0fv  5240  funopfv  5245  fnopfvb  5247  fvmptss2  5279  funfvbrb  5312  dff3im  5344  dff4im  5345  f1ompt  5352  idref  5428  foeqcnvco  5461  f1eqcocnv  5462  fliftel  5464  fliftel1  5465  fliftcnv  5466  f1oiso  5496  ovprc  5571  brabvv  5582  1st2ndbr  5841  xporderlem  5883  isprmpt2  5892  ottposg  5904  dftpos3  5911  dftpos4  5912  tposoprab  5929  tfrlem7  5966  tfrexlem  5983  ercnv  6193  brdifun  6199  swoord1  6201  swoord2  6202  0er  6206  elecg  6210  iinerm  6244  brecop  6262  idssen  6324  xpcomco  6370  ltdfpr  6758  xrlenlt  7244  frecuzrdgtcl  9494  frecuzrdgfunlem  9501  climcau  10322  divides  10342
  Copyright terms: Public domain W3C validator