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 5040 | . 2 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) | |
2 | opelxp 5572 | . 2 ⊢ (〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷) ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) | |
3 | 1, 2 | bitri 278 | 1 ⊢ (𝐴(𝐶 × 𝐷)𝐵 ↔ (𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 ∈ wcel 2112 〈cop 4533 class class class wbr 5039 × cxp 5534 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 ax-sep 5177 ax-nul 5184 ax-pr 5307 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-ral 3056 df-rex 3057 df-rab 3060 df-v 3400 df-dif 3856 df-un 3858 df-nul 4224 df-if 4426 df-sn 4528 df-pr 4530 df-op 4534 df-br 5040 df-opab 5102 df-xp 5542 |
This theorem is referenced by: brrelex12 5586 brel 5599 brinxp2 5611 eqbrrdva 5723 ssrelrn 5748 xpidtr 5967 xpco 6132 isocnv3 7119 tpostpos 7966 swoer 8399 erinxp 8451 ecopover 8481 infxpenlem 9592 fpwwe2lem5 10214 fpwwe2lem6 10215 fpwwe2lem8 10217 fpwwe2lem11 10220 fpwwe2lem12 10221 fpwwe2 10222 ltxrlt 10868 ltxr 12672 xpcogend 14502 invfuc 17437 elhoma 17492 efglem 19060 gsumcom3fi 19318 gsumdixp 19581 znleval 20473 gsumbagdiagOLD 20852 psrass1lemOLD 20853 gsumbagdiag 20855 psrass1lem 20856 opsrtoslem2 20967 brelg 30622 posrasymb 30916 trleile 30922 ecxpid 31224 qusxpid 31227 metider 31512 satefvfmla1 33054 mclsppslem 33212 xpab 33346 dfpo2 33392 slenlt 33641 dfon3 33880 brbigcup 33886 brsingle 33905 brimage 33914 brcart 33920 brapply 33926 brcup 33927 brcap 33928 funpartlem 33930 dfrdg4 33939 brub 33942 bj-xpcossxp 35044 itg2gt0cn 35518 grucollcld 41492 grumnud 41518 |
Copyright terms: Public domain | W3C validator |