![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > brabg | Unicode version |
Description: The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 19-Dec-2013.) |
Ref | Expression |
---|---|
opelopabg.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
opelopabg.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
brabg.5 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
brabg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelopabg.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | opelopabg.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sylan9bb 681 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | brabg.5 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | brabga 4433 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem is referenced by: brab 4441 ideqg 4987 opelcnvg 5015 f1owe 6036 brrpssg 6487 bren 7080 brdomg 7081 brwdom 7495 ltprord 8867 shftfib 11846 efgrelexlema 15340 cmbr 23043 leopg 23582 cvbr 23742 mdbr 23754 dmdbr 23759 soseq 25472 sltval 25519 axcontlem5 25815 isfne 26242 isref 26253 brabg2 26311 isriscg 26494 isfrgra 28098 lcvbr 29508 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2389 ax-sep 4294 ax-nul 4302 ax-pr 4367 |
This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2262 df-mo 2263 df-clab 2395 df-cleq 2401 df-clel 2404 df-nfc 2533 df-ne 2573 df-rab 2679 df-v 2922 df-dif 3287 df-un 3289 df-in 3291 df-ss 3298 df-nul 3593 df-if 3704 df-sn 3784 df-pr 3785 df-op 3787 df-br 4177 df-opab 4231 |
Copyright terms: Public domain | W3C validator |