![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brxp | Structured version Visualization version GIF version |
Description: Binary relation on a Cartesian product. (Contributed by NM, 22-Apr-2004.) |
Ref | Expression |
---|---|
brxp | ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-br 4924 | . 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) | |
2 | opelxp 5436 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | |
3 | 1, 2 | bitri 267 | 1 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 387 ∈ wcel 2048 〈cop 4441 class class class wbr 4923 × cxp 5398 |
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 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-ext 2745 ax-sep 5054 ax-nul 5061 ax-pr 5180 |
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 2014 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-br 4924 df-opab 4986 df-xp 5406 |
This theorem is referenced by: brrelex12 5447 brel 5460 brinxp2 5472 eqbrrdva 5583 ssrelrn 5606 xpidtr 5816 xpco 5972 isocnv3 6902 tpostpos 7708 swoer 8111 erinxp 8163 ecopover 8193 infxpenlem 9225 fpwwe2lem6 9847 fpwwe2lem7 9848 fpwwe2lem9 9850 fpwwe2lem12 9853 fpwwe2lem13 9854 fpwwe2 9855 ltxrlt 10503 ltxr 12320 xpcogend 14185 xpsfrnel2 16684 invfuc 17092 elhoma 17140 efglem 18590 gsumdixp 19072 gsumbagdiag 19860 psrass1lem 19861 opsrtoslem2 19968 znleval 20393 gsumcom3fi 20703 brelg 30114 posrasymb 30354 trleile 30363 metider 30735 mclsppslem 32290 dfpo2 32451 slenlt 32692 dfon3 32814 brbigcup 32820 brsingle 32839 brimage 32848 brcart 32854 brapply 32860 brcup 32861 brcap 32862 funpartlem 32864 dfrdg4 32873 brub 32876 itg2gt0cn 34336 grucollcld 39916 grumnud 39942 |
Copyright terms: Public domain | W3C validator |