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 5585 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → 〈𝐴, 𝐵〉 ∈ (𝐶 × 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 〈cop 4563 × cxp 5546 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 ax-nul 5201 ax-pr 5320 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-ral 3140 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-opab 5120 df-xp 5554 |
This theorem is referenced by: otel3xp 5592 opabssxpd 5782 fpr2g 6965 fliftrel 7050 elovimad 7193 el2xptp0 7725 oprab2co 7781 1stconst 7784 2ndconst 7785 curry2 7791 fsplitfpar 7803 offsplitfpar 7804 fnwelem 7814 xpf1o 8667 xpmapenlem 8672 unxpdomlem3 8712 fseqenlem1 9438 fseqenlem2 9439 iundom2g 9950 ordpipq 10352 addpqf 10354 mulpqf 10356 recmulnq 10374 ltexnq 10385 axmulf 10556 cnrecnv 14512 ruclem1 15572 eucalgf 15915 qredeu 15990 crth 16103 phimullem 16104 prmreclem3 16242 setsstruct2 16509 imasaddflem 16791 xpsaddlem 16834 xpsvsca 16838 xpsle 16840 comffval 16957 oppccofval 16974 isoval 17023 brcic 17056 funcf2 17126 idfu2nd 17135 resf2nd 17153 wunfunc 17157 homaval 17279 setcco 17331 catcco 17349 estrcco 17368 xpcco 17421 xpchom2 17424 xpcco2 17425 xpccatid 17426 prfcl 17441 prf1st 17442 prf2nd 17443 evlf2 17456 curf1cl 17466 curf2cl 17469 curfcl 17470 uncf1 17474 uncf2 17475 uncfcurf 17477 diag11 17481 diag12 17482 diag2 17483 curf2ndf 17485 hof2fval 17493 yonedalem21 17511 yonedalem22 17516 yonedalem3b 17517 yonffthlem 17520 latcl2 17646 lsmhash 18760 frgpuplem 18827 mdetrlin 21139 mdetrsca 21140 txcls 22140 txcnp 22156 txcnmpt 22160 txdis1cn 22171 txlly 22172 txnlly 22173 txlm 22184 lmcn2 22185 txkgen 22188 xkococnlem 22195 txhmeo 22339 ptuncnv 22343 txflf 22542 flfcnp2 22543 tmdcn2 22625 qustgplem 22656 tsmsadd 22682 imasdsf1olem 22910 xpsdsval 22918 comet 23050 metustid 23091 metustexhalf 23093 metuel2 23102 tngnm 23187 cnheiborlem 23485 bcthlem5 23858 ovollb2lem 24016 ovolctb 24018 ovoliunlem2 24031 ovolshftlem1 24037 ovolscalem1 24041 ovolicc1 24044 ioombl1lem1 24086 dyadf 24119 itg1addlem4 24227 limccnp2 24417 dvaddbr 24462 dvmulbr 24463 dvcobr 24470 lhop1lem 24537 cxpcn3 25256 dvdsmulf1o 25698 addsqnreup 25946 tgjustc1 26188 tgjustc2 26189 tgelrnln 26343 numclwwlk1lem2f 28061 ofresid 30317 fsuppcurry1 30387 fsuppcurry2 30388 prsdm 31056 prsrn 31057 esum2dlem 31250 hgt750lemb 31826 cvmlift2lem10 32456 goelel3xp 32492 sat1el2xp 32523 fmla0xp 32527 prv1n 32575 pprodss4v 33242 mblfinlem2 34811 projf1o 41335 ovolval4lem1 42808 ovolval5lem2 42812 |
Copyright terms: Public domain | W3C validator |