![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > brres | Structured version Unicode version |
Description: Binary relation on a restriction. (Contributed by NM, 12-Dec-2006.) |
Ref | Expression |
---|---|
opelres.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
brres |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelres.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | opelres 5200 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-br 4377 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-br 4377 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | anbi1i 695 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 3, 5 | 3bitr4i 277 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1709 ax-7 1729 ax-9 1761 ax-10 1776 ax-11 1781 ax-12 1793 ax-13 1944 ax-ext 2429 ax-sep 4497 ax-nul 4505 ax-pr 4615 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1702 df-clab 2436 df-cleq 2442 df-clel 2445 df-nfc 2598 df-ne 2643 df-ral 2797 df-rex 2798 df-rab 2801 df-v 3056 df-dif 3415 df-un 3417 df-in 3419 df-ss 3426 df-nul 3722 df-if 3876 df-sn 3962 df-pr 3964 df-op 3968 df-br 4377 df-opab 4435 df-xp 4930 df-res 4936 |
This theorem is referenced by: dfres2 5242 dfima2 5255 poirr2 5306 cores 5425 resco 5426 rnco 5428 fnres 5611 fvres 5789 nfunsn 5806 1stconst 6747 2ndconst 6748 fsplit 6763 dprd2da 16632 metustidOLD 20236 metustid 20237 dvres 21488 dvres2 21489 axhcompl-zf 24521 hlimadd 24716 hhcmpl 24723 hhcms 24726 hlim0 24759 dfpo2 27685 dfdm5 27707 dfrn5 27708 wfrlem5 27848 frrlem5 27892 txpss3v 28029 brtxp 28031 pprodss4v 28035 brpprod 28036 brimg 28088 brapply 28089 funpartfun 28094 dfrdg4 28101 funressnfv 30158 dfdfat2 30161 |
Copyright terms: Public domain | W3C validator |