MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  brres Structured version   Visualization version   GIF version

Theorem brres 5986
Description: Binary relation on a restriction. (Contributed by Mario Carneiro, 4-Nov-2015.) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022.)
Assertion
Ref Expression
brres (𝐶𝑉 → (𝐵(𝑅𝐴)𝐶 ↔ (𝐵𝐴𝐵𝑅𝐶)))

Proof of Theorem brres
StepHypRef Expression
1 opelres 5985 . 2 (𝐶𝑉 → (⟨𝐵, 𝐶⟩ ∈ (𝑅𝐴) ↔ (𝐵𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝑅)))
2 df-br 5148 . 2 (𝐵(𝑅𝐴)𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ (𝑅𝐴))
3 df-br 5148 . . 3 (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
43anbi2i 623 . 2 ((𝐵𝐴𝐵𝑅𝐶) ↔ (𝐵𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
51, 2, 43bitr4g 313 1 (𝐶𝑉 → (𝐵(𝑅𝐴)𝐶 ↔ (𝐵𝐴𝐵𝑅𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wcel 2106  cop 4633   class class class wbr 5147  cres 5677
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-res 5687
This theorem is referenced by:  brresi  5988  dfima2  6059  predres  6337  ttrclselem2  9717  axhcompl-zf  30238  fv1stcnv  34736  fv2ndcnv  34737  bj-idreseq  36031  bj-idreseqb  36032  brcnvepres  37123  brres2  37124  eldmres  37126  elrnres  37127  elecres  37133  brinxprnres  37148  exanres  37152  eqres  37197  alrmomorn  37215  alrmomodm  37216  brxrn  37232  rnxrnres  37257  1cossres  37287  brressn  37299  eldm1cossres  37318  brssrres  37362  disjres  37602  antisymrelres  37621  dfdfat2  45822
  Copyright terms: Public domain W3C validator