![]() |
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 4805 | . 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) | |
2 | opelxp 5303 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | |
3 | 1, 2 | bitri 264 | 1 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 ∈ wcel 2139 〈cop 4327 class class class wbr 4804 × cxp 5264 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-sep 4933 ax-nul 4941 ax-pr 5055 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ral 3055 df-rex 3056 df-rab 3059 df-v 3342 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 df-if 4231 df-sn 4322 df-pr 4324 df-op 4328 df-br 4805 df-opab 4865 df-xp 5272 |
This theorem is referenced by: brrelex12 5312 brel 5325 brinxp2 5337 eqbrrdva 5447 ssrelrn 5470 xpidtr 5676 xpco 5836 isocnv3 6746 tpostpos 7542 swoer 7943 erinxp 7990 ecopover 8020 infxpenlem 9046 fpwwe2lem6 9669 fpwwe2lem7 9670 fpwwe2lem9 9672 fpwwe2lem12 9675 fpwwe2lem13 9676 fpwwe2 9677 ltxrlt 10320 ltxr 12162 xpcogend 13934 xpsfrnel2 16447 invfuc 16855 elhoma 16903 efglem 18349 gsumdixp 18829 gsumbagdiag 19598 psrass1lem 19599 opsrtoslem2 19707 znleval 20125 gsumcom3fi 20428 brelg 29749 posrasymb 29987 trleile 29996 metider 30267 mclsppslem 31808 dfpo2 31973 slenlt 32204 dfon3 32326 brbigcup 32332 brsingle 32351 brimage 32360 brcart 32366 brapply 32372 brcup 32373 brcap 32374 funpartlem 32376 dfrdg4 32385 brub 32388 itg2gt0cn 33796 brinxp2ALTV 34376 |
Copyright terms: Public domain | W3C validator |