![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opelxpd | Structured version Visualization version GIF version |
Description: Ordered pair membership in a Cartesian product, deduction form. (Contributed by Glauco Siliprandi, 3-Mar-2021.) |
Ref | Expression |
---|---|
opelxpd.1 | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
opelxpd.2 | ⊢ (𝜑 → 𝐵 ∈ 𝐷) |
Ref | Expression |
---|---|
opelxpd | ⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opelxpd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶) | |
2 | opelxpd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝐷) | |
3 | opelxpi 5487 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2083 〈cop 4484 × cxp 5448 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-ext 2771 ax-sep 5101 ax-nul 5108 ax-pr 5228 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ral 3112 df-rex 3113 df-rab 3116 df-v 3442 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-nul 4218 df-if 4388 df-sn 4479 df-pr 4481 df-op 4485 df-opab 5031 df-xp 5456 |
This theorem is referenced by: otel3xp 5494 opabssxpd 5682 fpr2g 6847 fliftrel 6931 elovimad 7070 el2xptp0 7599 oprab2co 7655 1stconst 7658 2ndconst 7659 curry2 7665 fnwelem 7685 xpf1o 8533 xpmapenlem 8538 unxpdomlem3 8577 fseqenlem1 9303 fseqenlem2 9304 iundom2g 9815 ordpipq 10217 addpqf 10219 mulpqf 10221 recmulnq 10239 ltexnq 10250 axmulf 10421 cnrecnv 14362 ruclem1 15421 eucalgf 15760 qredeu 15835 crth 15948 phimullem 15949 prmreclem3 16087 setsstruct2 16354 imasaddflem 16636 xpsaddlem 16679 xpsvsca 16683 xpsle 16685 comffval 16802 oppccofval 16819 isoval 16868 brcic 16901 funcf2 16971 idfu2nd 16980 resf2nd 16998 wunfunc 17002 homaval 17124 setcco 17176 catcco 17194 estrcco 17213 xpcco 17266 xpchom2 17269 xpcco2 17270 xpccatid 17271 prfcl 17286 prf1st 17287 prf2nd 17288 evlf2 17301 curf1cl 17311 curf2cl 17314 curfcl 17315 uncf1 17319 uncf2 17320 uncfcurf 17322 diag11 17326 diag12 17327 diag2 17328 curf2ndf 17330 hof2fval 17338 yonedalem21 17356 yonedalem22 17361 yonedalem3b 17362 yonffthlem 17365 latcl2 17491 lsmhash 18562 frgpuplem 18629 mdetrlin 20899 mdetrsca 20900 txcls 21900 txcnp 21916 txcnmpt 21920 txdis1cn 21931 txlly 21932 txnlly 21933 txlm 21944 lmcn2 21945 txkgen 21948 xkococnlem 21955 txhmeo 22099 ptuncnv 22103 txflf 22302 flfcnp2 22303 tmdcn2 22385 qustgplem 22416 tsmsadd 22442 imasdsf1olem 22670 xpsdsval 22678 comet 22810 metustid 22851 metustexhalf 22853 metuel2 22862 tngnm 22947 cnheiborlem 23245 bcthlem5 23618 ovollb2lem 23776 ovolctb 23778 ovoliunlem2 23791 ovolshftlem1 23797 ovolscalem1 23801 ovolicc1 23804 ioombl1lem1 23846 dyadf 23879 itg1addlem4 23987 limccnp2 24177 dvaddbr 24222 dvmulbr 24223 dvcobr 24230 lhop1lem 24297 cxpcn3 25014 dvdsmulf1o 25457 addsqnreup 25705 tgjustc1 25947 tgjustc2 25948 tgelrnln 26102 numclwwlk1lem2f 27822 ofresid 30075 fsuppcurry1 30145 fsuppcurry2 30146 prsdm 30770 prsrn 30771 esum2dlem 30964 hgt750lemb 31540 cvmlift2lem10 32169 goelel3xp 32205 sat1el2xp 32236 fmla0xp 32240 prv1n 32288 pprodss4v 32956 mblfinlem2 34482 projf1o 41020 ovolval4lem1 42495 ovolval5lem2 42499 |
Copyright terms: Public domain | W3C validator |