![]() |
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 5106 | . 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) | |
2 | opelxp 5669 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | |
3 | 1, 2 | bitri 274 | 1 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 ∈ wcel 2106 〈cop 4592 class class class wbr 5105 × cxp 5631 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-br 5106 df-opab 5168 df-xp 5639 |
This theorem is referenced by: brrelex12 5684 brel 5697 brinxp2 5709 eqbrrdva 5825 ssrelrn 5850 xpidtr 6076 xpco 6241 dfpo2 6248 predtrss 6276 isocnv3 7276 tpostpos 8176 swoer 8677 erinxp 8729 ecopover 8759 infxpenlem 9948 fpwwe2lem5 10570 fpwwe2lem6 10571 fpwwe2lem8 10573 fpwwe2lem11 10576 fpwwe2lem12 10577 fpwwe2 10578 ltxrlt 11224 ltxr 13035 xpcogend 14858 invfuc 17862 elhoma 17917 efglem 19496 gsumcom3fi 19754 gsumdixp 20031 znleval 20959 gsumbagdiagOLD 21339 psrass1lemOLD 21340 gsumbagdiag 21342 psrass1lem 21343 opsrtoslem2 21461 slenlt 27098 brelg 31475 posrasymb 31769 trleile 31775 ecxpid 32092 qusxpid 32095 metider 32415 satefvfmla1 33959 mclsppslem 34117 xpab 34237 dfon3 34467 brbigcup 34473 brsingle 34492 brimage 34501 brcart 34507 brapply 34513 brcup 34514 brcap 34515 funpartlem 34517 dfrdg4 34526 brub 34529 bj-xpcossxp 35650 itg2gt0cn 36123 grucollcld 42521 grumnud 42547 |
Copyright terms: Public domain | W3C validator |