![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brres | Structured version Visualization 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 5110 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-br 4403 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-br 4403 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | anbi1i 701 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 2, 3, 5 | 3bitr4i 281 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pr 4639 |
This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-ral 2742 df-rex 2743 df-rab 2746 df-v 3047 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-nul 3732 df-if 3882 df-sn 3969 df-pr 3971 df-op 3975 df-br 4403 df-opab 4462 df-xp 4840 df-res 4846 |
This theorem is referenced by: dfres2 5157 dfima2 5170 poirr2 5224 cores 5338 resco 5339 rnco 5341 fnres 5692 fvres 5879 nfunsn 5896 1stconst 6884 2ndconst 6885 fsplit 6901 wfrlem5 7040 dprd2da 17675 metustid 21569 dvres 22866 dvres2 22867 ltgov 24642 axhcompl-zf 26651 hlimadd 26846 hhcmpl 26853 hhcms 26856 hlim0 26888 dfpo2 30395 dfdm5 30418 dfrn5 30419 frrlem5 30518 txpss3v 30645 brtxp 30647 pprodss4v 30651 brpprod 30652 brimg 30704 brapply 30705 funpartfun 30710 dfrdg4 30718 funressnfv 38629 dfdfat2 38633 |
Copyright terms: Public domain | W3C validator |