![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 1st2nd2 | Structured version Visualization version GIF version |
Description: Reconstruction of a member of a Cartesian product in terms of its ordered pair components. (Contributed by NM, 20-Oct-2013.) |
Ref | Expression |
---|---|
1st2nd2 | ⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elxp6 7350 | . 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶))) | |
2 | 1 | simplbi 481 | 1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 = wceq 1631 ∈ wcel 2145 〈cop 4323 × cxp 5248 ‘cfv 6032 1st c1st 7314 2nd c2nd 7315 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4916 ax-nul 4924 ax-pow 4975 ax-pr 5035 ax-un 7097 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-sbc 3589 df-dif 3727 df-un 3729 df-in 3731 df-ss 3738 df-nul 4065 df-if 4227 df-sn 4318 df-pr 4320 df-op 4324 df-uni 4576 df-br 4788 df-opab 4848 df-mpt 4865 df-id 5158 df-xp 5256 df-rel 5257 df-cnv 5258 df-co 5259 df-dm 5260 df-rn 5261 df-iota 5995 df-fun 6034 df-fv 6040 df-1st 7316 df-2nd 7317 |
This theorem is referenced by: 1st2ndb 7356 xpopth 7357 eqop 7358 2nd1st 7363 1st2nd 7364 opiota 7379 disjen 8274 xpmapenlem 8284 mapunen 8286 djulf1o 8939 djurf1o 8940 djur 8946 r0weon 9036 enqbreq2 9945 nqereu 9954 lterpq 9995 elreal2 10156 cnref1o 12031 ruclem6 15171 ruclem8 15173 ruclem9 15174 ruclem12 15177 eucalgval 15504 eucalginv 15506 eucalglt 15507 eucalg 15509 qnumdenbi 15660 isstruct2 16075 xpsff1o 16437 comfffval2 16569 comfeq 16574 idfucl 16749 funcpropd 16768 coapm 16929 xpccatid 17037 1stfcl 17046 2ndfcl 17047 1st2ndprf 17055 xpcpropd 17057 evlfcl 17071 hofcl 17108 hofpropd 17116 yonedalem3 17129 gsum2dlem2 18578 mdetunilem9 20645 tx1cn 21634 tx2cn 21635 txdis 21657 txlly 21661 txnlly 21662 txhaus 21672 txkgen 21677 txconn 21714 utop3cls 22276 ucnima 22306 fmucndlem 22316 psmetxrge0 22339 imasdsf1olem 22399 cnheiborlem 22974 caublcls 23327 bcthlem1 23341 bcthlem2 23342 bcthlem4 23344 bcthlem5 23345 ovolfcl 23455 ovolfioo 23456 ovolficc 23457 ovolficcss 23458 ovolfsval 23459 ovolicc2lem1 23506 ovolicc2lem5 23510 ovolfs2 23560 uniiccdif 23567 uniioovol 23568 uniiccvol 23569 uniioombllem2a 23571 uniioombllem2 23572 uniioombllem3a 23573 uniioombllem3 23574 uniioombllem4 23575 uniioombllem5 23576 uniioombllem6 23577 dyadmbl 23589 fsumvma 25160 ofpreima 29806 ofpreima2 29807 fimaproj 30241 1stmbfm 30663 2ndmbfm 30664 sibfof 30743 oddpwdcv 30758 txsconnlem 31561 mpst123 31776 bj-elid 33423 poimirlem4 33747 poimirlem26 33769 poimirlem27 33770 mblfinlem1 33780 mblfinlem2 33781 ftc2nc 33827 heiborlem8 33950 dvhgrp 36918 dvhlveclem 36919 fvovco 39902 dvnprodlem1 40680 volioof 40722 fvvolioof 40724 fvvolicof 40726 etransclem44 41013 ovolval3 41382 ovolval4lem1 41384 ovolval5lem2 41388 ovnovollem1 41391 ovnovollem2 41392 smfpimbor1lem1 41526 |
Copyright terms: Public domain | W3C validator |