Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > brresi | Structured version Visualization version GIF version |
Description: Binary relation on a restriction. (Contributed by NM, 12-Dec-2006.) |
Ref | Expression |
---|---|
opelresi.1 | ⊢ 𝐶 ∈ V |
Ref | Expression |
---|---|
brresi | ⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelresi.1 | . 2 ⊢ 𝐶 ∈ V | |
2 | brres 5853 | . 2 ⊢ (𝐶 ∈ V → (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 ∧ wa 396 ∈ wcel 2105 Vcvv 3492 class class class wbr 5057 ↾ cres 5550 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-br 5058 df-opab 5120 df-xp 5554 df-res 5560 |
This theorem is referenced by: dfres2 5902 poirr2 5977 cores 6095 resco 6096 rnco 6098 fnres 6467 fvres 6682 nfunsn 6700 1stconst 7784 2ndconst 7785 fsplit 7801 fsplitOLD 7802 wfrlem5 7948 dprd2da 19093 metustid 23091 dvres 24436 dvres2 24437 ltgov 26310 hlimadd 28897 hhcmpl 28904 hhcms 28907 hlim0 28939 dfpo2 32888 eqfunresadj 32901 dfdm5 32913 dfrn5 32914 fprlem1 33034 frrlem15 33039 txpss3v 33236 brtxp 33238 pprodss4v 33242 brpprod 33243 brimg 33295 brapply 33296 funpartfun 33301 dfrdg4 33309 xrnss3v 35504 funressnfv 43155 funressnvmo 43157 afv2res 43315 setrec2lem2 44725 |
Copyright terms: Public domain | W3C validator |