| 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 8048 | . 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶))) | |
| 2 | 1 | simplbi 497 | 1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 〈cop 4632 × cxp 5683 ‘cfv 6561 1st c1st 8012 2nd c2nd 8013 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-iota 6514 df-fun 6563 df-fv 6569 df-1st 8014 df-2nd 8015 |
| This theorem is referenced by: 1st2ndb 8054 xpopth 8055 eqop 8056 2nd1st 8063 1st2nd 8064 opiota 8084 fimaproj 8160 disjen 9174 xpmapenlem 9184 mapunen 9186 djulf1o 9952 djurf1o 9953 djur 9959 r0weon 10052 enqbreq2 10960 nqereu 10969 lterpq 11010 elreal2 11172 cnref1o 13027 ruclem6 16271 ruclem8 16273 ruclem9 16274 ruclem12 16277 eucalgval 16619 eucalginv 16621 eucalglt 16622 eucalg 16624 qnumdenbi 16781 isstruct2 17186 xpsff1o 17612 comfffval2 17744 comfeq 17749 idfucl 17926 funcpropd 17947 coapm 18116 xpccatid 18233 1stfcl 18242 2ndfcl 18243 1st2ndprf 18251 xpcpropd 18253 evlfcl 18267 hofcl 18304 hofpropd 18312 yonedalem3 18325 gsum2dlem2 19989 mdetunilem9 22626 tx1cn 23617 tx2cn 23618 txdis 23640 txlly 23644 txnlly 23645 txhaus 23655 txkgen 23660 txconn 23697 utop3cls 24260 ucnima 24290 fmucndlem 24300 psmetxrge0 24323 imasdsf1olem 24383 cnheiborlem 24986 caublcls 25343 bcthlem1 25358 bcthlem2 25359 bcthlem4 25361 bcthlem5 25362 ovolfcl 25501 ovolfioo 25502 ovolficc 25503 ovolficcss 25504 ovolfsval 25505 ovolicc2lem1 25552 ovolicc2lem5 25556 ovolfs2 25606 uniiccdif 25613 uniioovol 25614 uniiccvol 25615 uniioombllem2a 25617 uniioombllem2 25618 uniioombllem3a 25619 uniioombllem3 25620 uniioombllem4 25621 uniioombllem5 25622 uniioombllem6 25623 dyadmbl 25635 fsumvma 27257 opreu2reuALT 32496 ofpreima 32675 ofpreima2 32676 elrgspnsubrunlem2 33252 erler 33269 1stmbfm 34262 2ndmbfm 34263 sibfof 34342 oddpwdcv 34357 txsconnlem 35245 mpst123 35545 bj-elid4 37169 bj-elid6 37171 poimirlem4 37631 poimirlem26 37653 poimirlem27 37654 mblfinlem1 37664 mblfinlem2 37665 ftc2nc 37709 heiborlem8 37825 dvhgrp 41109 dvhlveclem 41110 fvovco 45198 dvnprodlem1 45961 volioof 46002 fvvolioof 46004 fvvolicof 46006 etransclem44 46293 ovolval3 46662 ovolval4lem1 46664 ovolval5lem2 46668 ovnovollem1 46671 ovnovollem2 46672 smfpimbor1lem1 46813 rrx2xpref1o 48639 swapf2f1oa 48983 swapfida 48986 swapffunca 48990 swapfiso 48991 cofuswapf1 48994 cofuswapf2 48995 fuco2eld2 49009 fuco11b 49032 fuco11bALT 49033 fucoco2 49053 fucofunca 49055 fucolid 49056 fucorid 49057 precofvalALT 49063 |
| Copyright terms: Public domain | W3C validator |