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 7200 | . 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ (𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∧ ((1st ‘𝐴) ∈ 𝐵 ∧ (2nd ‘𝐴) ∈ 𝐶))) | |
2 | 1 | simplbi 476 | 1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → 𝐴 = 〈(1st ‘𝐴), (2nd ‘𝐴)〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 384 = wceq 1483 ∈ wcel 1990 〈cop 4183 × cxp 5112 ‘cfv 5888 1st c1st 7166 2nd c2nd 7167 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-iota 5851 df-fun 5890 df-fv 5896 df-1st 7168 df-2nd 7169 |
This theorem is referenced by: 1st2ndb 7206 xpopth 7207 eqop 7208 2nd1st 7213 1st2nd 7214 opiota 7229 disjen 8117 xpmapenlem 8127 mapunen 8129 r0weon 8835 enqbreq2 9742 nqereu 9751 lterpq 9792 elreal2 9953 cnref1o 11827 ruclem6 14964 ruclem8 14966 ruclem9 14967 ruclem12 14970 eucalgval 15295 eucalginv 15297 eucalglt 15298 eucalg 15300 qnumdenbi 15452 isstruct2 15867 xpsff1o 16228 comfffval2 16361 comfeq 16366 idfucl 16541 funcpropd 16560 coapm 16721 xpccatid 16828 1stfcl 16837 2ndfcl 16838 1st2ndprf 16846 xpcpropd 16848 evlfcl 16862 hofcl 16899 hofpropd 16907 yonedalem3 16920 gsum2dlem2 18370 mdetunilem9 20426 tx1cn 21412 tx2cn 21413 txdis 21435 txlly 21439 txnlly 21440 txhaus 21450 txkgen 21455 txconn 21492 utop3cls 22055 ucnima 22085 fmucndlem 22095 psmetxrge0 22118 imasdsf1olem 22178 cnheiborlem 22753 caublcls 23107 bcthlem1 23121 bcthlem2 23122 bcthlem4 23124 bcthlem5 23125 ovolfcl 23235 ovolfioo 23236 ovolficc 23237 ovolficcss 23238 ovolfsval 23239 ovolicc2lem1 23285 ovolicc2lem5 23289 ovolfs2 23339 uniiccdif 23346 uniioovol 23347 uniiccvol 23348 uniioombllem2a 23350 uniioombllem2 23351 uniioombllem3a 23352 uniioombllem3 23353 uniioombllem4 23354 uniioombllem5 23355 uniioombllem6 23356 dyadmbl 23368 fsumvma 24938 ofpreima 29465 ofpreima2 29466 fimaproj 29900 1stmbfm 30322 2ndmbfm 30323 sibfof 30402 oddpwdcv 30417 txsconnlem 31222 mpst123 31437 bj-elid 33085 poimirlem4 33413 poimirlem26 33435 poimirlem27 33436 mblfinlem1 33446 mblfinlem2 33447 ftc2nc 33494 heiborlem8 33617 dvhgrp 36396 dvhlveclem 36397 fvovco 39381 dvnprodlem1 40161 volioof 40204 fvvolioof 40206 fvvolicof 40208 etransclem44 40495 ovolval3 40861 ovolval4lem1 40863 ovolval5lem2 40867 ovnovollem1 40870 ovnovollem2 40871 smfpimbor1lem1 41005 |
Copyright terms: Public domain | W3C validator |