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

Theorem brres 5733
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 5732 . 2 (𝐶𝑉 → (⟨𝐵, 𝐶⟩ ∈ (𝑅𝐴) ↔ (𝐵𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝑅)))
2 df-br 4957 . 2 (𝐵(𝑅𝐴)𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ (𝑅𝐴))
3 df-br 4957 . . 3 (𝐵𝑅𝐶 ↔ ⟨𝐵, 𝐶⟩ ∈ 𝑅)
43anbi2i 622 . 2 ((𝐵𝐴𝐵𝑅𝐶) ↔ (𝐵𝐴 ∧ ⟨𝐵, 𝐶⟩ ∈ 𝑅))
51, 2, 43bitr4g 315 1 (𝐶𝑉 → (𝐵(𝑅𝐴)𝐶 ↔ (𝐵𝐴𝐵𝑅𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wcel 2079  cop 4472   class class class wbr 4956  cres 5437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pr 5214
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-op 4473  df-br 4957  df-opab 5019  df-xp 5441  df-res 5447
This theorem is referenced by:  brresi  5735  dfima2  5800  axhcompl-zf  28454  fv1stcnv  32573  fv2ndcnv  32574  brcnvepres  35008  brres2  35009  eldmres  35010  elecres  35014  brinxprnres  35028  exanres  35032  eqres  35079  alrmomorn  35094  alrmomodm  35095  brxrn  35107  rnxrnres  35128  1cossres  35155  eldm1cossres  35181  brssrres  35225  dfdfat2  42797
  Copyright terms: Public domain W3C validator