![]() |
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 5992 | . 2 ⊢ (𝐶 ∈ V → (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 394 ∈ wcel 2098 Vcvv 3461 class class class wbr 5149 ↾ cres 5680 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 ax-nul 5307 ax-pr 5429 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 df-opab 5212 df-xp 5684 df-res 5690 |
This theorem is referenced by: dfres2 6046 poirr2 6131 cores 6255 resco 6256 rnco 6258 dfpo2 6302 fnres 6683 fvres 6915 nfunsn 6938 eqfunresadj 7367 1stconst 8105 2ndconst 8106 fsplit 8122 fprlem1 8306 wfrlem5OLD 8334 ttrclresv 9742 ttrclselem2 9751 frrlem15 9782 dprd2da 20011 metustid 24507 dvres 25884 dvres2 25885 ltgov 28473 hlimadd 31075 hhcmpl 31082 hhcms 31085 hlim0 31117 dfdm5 35499 dfrn5 35500 txpss3v 35605 brtxp 35607 pprodss4v 35611 brpprod 35612 brimg 35664 brapply 35665 funpartfun 35670 dfrdg4 35678 xrnss3v 37974 funressnfv 46563 funressnvmo 46565 afv2res 46757 setrec2lem2 48311 |
Copyright terms: Public domain | W3C validator |