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 5069 | . 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) | |
2 | opelxp 5593 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | |
3 | 1, 2 | bitri 277 | 1 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∈ wcel 2114 〈cop 4575 class class class wbr 5068 × cxp 5555 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pr 5332 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-rex 3146 df-rab 3149 df-v 3498 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-sn 4570 df-pr 4572 df-op 4576 df-br 5069 df-opab 5131 df-xp 5563 |
This theorem is referenced by: brrelex12 5606 brel 5619 brinxp2 5631 eqbrrdva 5742 ssrelrn 5765 xpidtr 5984 xpco 6142 isocnv3 7087 tpostpos 7914 swoer 8321 erinxp 8373 ecopover 8403 infxpenlem 9441 fpwwe2lem6 10059 fpwwe2lem7 10060 fpwwe2lem9 10062 fpwwe2lem12 10065 fpwwe2lem13 10066 fpwwe2 10067 ltxrlt 10713 ltxr 12513 xpcogend 14336 invfuc 17246 elhoma 17294 efglem 18844 gsumcom3fi 19101 gsumdixp 19361 gsumbagdiag 20158 psrass1lem 20159 opsrtoslem2 20267 znleval 20703 brelg 30362 posrasymb 30646 trleile 30655 ecxpid 30927 qusxpid 30930 metider 31136 satefvfmla1 32674 mclsppslem 32832 dfpo2 32993 slenlt 33233 dfon3 33355 brbigcup 33361 brsingle 33380 brimage 33389 brcart 33395 brapply 33401 brcup 33402 brcap 33403 funpartlem 33405 dfrdg4 33414 brub 33417 itg2gt0cn 34949 grucollcld 40603 grumnud 40629 |
Copyright terms: Public domain | W3C validator |