![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brxp | Structured version Visualization version Unicode version |
Description: Binary relation on a Cartesian product. (Contributed by NM, 22-Apr-2004.) |
Ref | Expression |
---|---|
brxp |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-br 4416 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | opelxp 4882 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | bitri 257 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pr 4652 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-rab 2757 df-v 3058 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-sn 3980 df-pr 3982 df-op 3986 df-br 4416 df-opab 4475 df-xp 4858 |
This theorem is referenced by: brrelex12 4890 brel 4901 brinxp2 4914 eqbrrdva 5022 xpidtr 5240 xpco 5394 isocnv3 6247 tpostpos 7018 swoer 7416 erinxp 7462 ecopover 7492 infxpenlem 8469 fpwwe2lem6 9085 fpwwe2lem7 9086 fpwwe2lem9 9088 fpwwe2lem12 9091 fpwwe2lem13 9092 fpwwe2 9093 ltxrlt 9729 ltxr 11443 xpcogend 13086 xpsfrnel2 15519 invfuc 15927 elhoma 15975 efglem 17414 gsumdixp 17885 gsumbagdiag 18648 psrass1lem 18649 opsrtoslem2 18756 znleval 19173 gsumcom3fi 19473 brelg 28265 posrasymb 28466 trleile 28475 metider 28745 mclsppslem 30269 dfpo2 30443 dfon3 30707 brbigcup 30713 brsingle 30732 brimage 30741 brcart 30747 brapply 30753 brcup 30754 brcap 30755 funpartlem 30757 dfrdg4 30766 brub 30769 itg2gt0cn 32041 ssrelrn 39051 |
Copyright terms: Public domain | W3C validator |