![]() |
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 5674 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷)) | |
4 | 1, 2, 3 | syl2anc 585 | 1 ⊢ (𝜑 → ⟨𝐴, 𝐵⟩ ∈ (𝐶 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 ⟨cop 4596 × cxp 5635 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-sep 5260 ax-nul 5267 ax-pr 5388 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-opab 5172 df-xp 5643 |
This theorem is referenced by: otel3xp 5682 opabssxpd 5683 relssdmrn 6224 fpr2g 7165 fliftrel 7257 elovimad 7409 el2xptp0 7972 oprab2co 8033 1stconst 8036 2ndconst 8037 curry2 8043 fsplitfpar 8054 offsplitfpar 8055 fnwelem 8067 xpf1o 9089 xpmapenlem 9094 unxpdomlem3 9202 fseqenlem1 9968 fseqenlem2 9969 iundom2g 10484 ordpipq 10886 addpqf 10888 mulpqf 10890 recmulnq 10908 ltexnq 10919 axmulf 11090 cnrecnv 15059 ruclem1 16121 eucalgf 16467 qredeu 16542 crth 16658 phimullem 16659 prmreclem3 16798 setsstruct2 17054 imasaddflem 17420 xpsaddlem 17463 xpsvsca 17467 xpsle 17469 comffval 17587 oppccofval 17605 isoval 17656 brcic 17689 funcf2 17762 idfu2nd 17771 resf2nd 17789 wunfunc 17793 wunfuncOLD 17794 homaval 17925 setcco 17977 catcco 17999 estrcco 18025 xpcco 18079 xpchom2 18082 xpcco2 18083 xpccatid 18084 prfcl 18099 prf1st 18100 prf2nd 18101 evlf2 18115 curf1cl 18125 curf2cl 18128 curfcl 18129 uncf1 18133 uncf2 18134 uncfcurf 18136 diag11 18140 diag12 18141 diag2 18142 curf2ndf 18144 hof2fval 18152 yonedalem21 18170 yonedalem22 18175 yonedalem3b 18176 yonffthlem 18179 latcl2 18333 lsmhash 19495 frgpuplem 19562 mdetrlin 21974 mdetrsca 21975 txcls 22978 txcnp 22994 txcnmpt 22998 txdis1cn 23009 txlly 23010 txnlly 23011 txlm 23022 lmcn2 23023 txkgen 23026 xkococnlem 23033 txhmeo 23177 ptuncnv 23181 txflf 23380 flfcnp2 23381 tmdcn2 23463 qustgplem 23495 tsmsadd 23521 imasdsf1olem 23749 xpsdsval 23757 comet 23892 metustid 23933 metustexhalf 23935 metuel2 23944 tngnm 24038 cnheiborlem 24340 bcthlem5 24715 ovollb2lem 24875 ovolctb 24877 ovoliunlem2 24890 ovolshftlem1 24896 ovolscalem1 24900 ovolicc1 24903 ioombl1lem1 24945 dyadf 24978 itg1addlem4 25086 itg1addlem4OLD 25087 limccnp2 25279 dvaddbr 25325 dvmulbr 25326 dvcobr 25333 lhop1lem 25400 cxpcn3 26124 dvdsmulf1o 26566 addsqnreup 26814 addsval 27303 mulsval 27403 tgjustc1 27466 tgjustc2 27467 tgelrnln 27621 numclwwlk1lem2f 29348 ofresid 31611 fsuppcurry1 31696 fsuppcurry2 31697 gsumpart 31953 prsdm 32559 prsrn 32560 esum2dlem 32755 hgt750lemb 33333 cvmlift2lem10 33970 goelel3xp 34006 sat1el2xp 34037 fmla0xp 34041 prv1n 34089 pprodss4v 34522 poimirlem3 36131 poimirlem4 36132 poimirlem17 36145 poimirlem20 36148 mblfinlem2 36166 projf1o 43509 ovolval4lem1 44980 ovolval5lem2 44984 |
Copyright terms: Public domain | W3C validator |