![]() |
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 5703 | . 2 ⊢ (𝐶 ∈ V → (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐵(𝑅 ↾ 𝐴)𝐶 ↔ (𝐵 ∈ 𝐴 ∧ 𝐵𝑅𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 387 ∈ wcel 2050 Vcvv 3415 class class class wbr 4930 ↾ cres 5410 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pr 5187 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-sn 4443 df-pr 4445 df-op 4449 df-br 4931 df-opab 4993 df-xp 5414 df-res 5420 |
This theorem is referenced by: dfres2 5756 poirr2 5826 cores 5943 resco 5944 rnco 5946 fnres 6308 fvres 6520 nfunsn 6539 1stconst 7605 2ndconst 7606 fsplit 7622 wfrlem5 7765 dprd2da 18917 metustid 22870 dvres 24215 dvres2 24216 ltgov 26088 hlimadd 28752 hhcmpl 28759 hhcms 28762 hlim0 28794 dfpo2 32511 eqfunresadj 32524 dfdm5 32536 dfrn5 32537 fprlem1 32658 frrlem15 32663 txpss3v 32860 brtxp 32862 pprodss4v 32866 brpprod 32867 brimg 32919 brapply 32920 funpartfun 32925 dfrdg4 32933 xrnss3v 35069 funressnfv 42684 funressnvmo 42686 afv2res 42845 setrec2lem2 44165 |
Copyright terms: Public domain | W3C validator |