![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brres | Structured version Visualization version GIF version |
Description: Binary relation on a restriction. (Contributed by Mario Carneiro, 4-Nov-2015.) Commute the consequent. (Revised by Peter Mazsa, 24-Sep-2022.) |
Ref | Expression |
---|---|
brres | ⊢ (𝐶 ∈ 𝑉 → (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelres 5732 | . 2 ⊢ (𝐶 ∈ 𝑉 → (〈𝐵, 𝐶〉 ∈ (𝑅 ↾ 𝐴) ↔ (𝐵 ∈ 𝐴 ∧ 〈𝐵, 𝐶〉 ∈ 𝑅))) | |
2 | df-br 4957 | . 2 ⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ 〈𝐵, 𝐶〉 ∈ (𝑅 ↾ 𝐴)) | |
3 | df-br 4957 | . . 3 ⊢ (𝐵𝑅𝐶 ↔ 〈𝐵, 𝐶〉 ∈ 𝑅) | |
4 | 3 | anbi2i 622 | . 2 ⊢ ((𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶) ↔ (𝐵 ∈ 𝐴 ∧ 〈𝐵, 𝐶〉 ∈ 𝑅)) |
5 | 1, 2, 4 | 3bitr4g 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 |