xp2nd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xp2nd		Structured version Visualization version GIF version

Theorem xp2nd 8036

Description: Location of the second element of a Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)

**Assertion**
Ref	Expression
xp2nd	⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2^nd ‘𝐴) ∈ 𝐶)

Proof of Theorem xp2nd Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp 5705	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3466	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3466	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 8014	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2^nd ‘𝐴) = 𝑐)
5	4	eleq1d 2811	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2^nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 476	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2^nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 714	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2^nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1928	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2^nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2^nd ‘𝐴) ∈ 𝐶)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 ∃wex 1774 ∈ wcel 2099 ⟨cop 4639 × cxp 5680 ‘cfv 6554 2^nd c2nd 8002

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-sep 5304 ax-nul 5311 ax-pr 5433 ax-un 7746

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-opab 5216 df-mpt 5237 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-iota 6506 df-fun 6556 df-fv 6562 df-2nd 8004

This theorem is referenced by: offval22 8102 fimaproj 8149 disjen 9172 xpf1o 9177 xpmapenlem 9182 mapunen 9184 djur 9962 r0weon 10055 infxpenlem 10056 fseqdom 10069 axcc2lem 10479 iunfo 10582 iundom2g 10583 enqbreq2 10963 nqereu 10972 addpqf 10987 mulpqf 10989 adderpqlem 10997 mulerpqlem 10998 addassnq 11001 mulassnq 11002 distrnq 11004 mulidnq 11006 recmulnq 11007 ltsonq 11012 lterpq 11013 ltanq 11014 ltmnq 11015 ltexnq 11018 archnq 11023 elreal2 11175 cnref1o 13021 fsumcom2 15778 fprodcom2 15986 ruclem6 16237 ruclem8 16239 ruclem9 16240 ruclem10 16241 ruclem12 16243 eucalgval 16583 eucalginv 16585 eucalglt 16586 eucalgcvga 16587 eucalg 16588 xpsff1o 17582 comfffval2 17714 comfeq 17719 idfucl 17900 funcpropd 17922 fucpropd 18002 xpccatid 18212 1stfcl 18221 2ndfcl 18222 xpcpropd 18233 hofcl 18284 hofpropd 18292 yonedalem3 18305 lsmhash 19703 gsum2dlem2 19969 dprd2da 20042 evlslem4 22089 mdetunilem9 22613 tx1cn 23604 txdis 23627 txlly 23631 txnlly 23632 txhaus 23642 txkgen 23647 txconn 23684 txhmeo 23798 ptuncnv 23802 ptunhmeo 23803 xkohmeo 23810 utop2nei 24246 utop3cls 24247 imasdsf1olem 24370 cnheiborlem 24971 caubl 25327 caublcls 25328 bcthlem2 25344 bcthlem4 25346 bcthlem5 25347 ovolficcss 25489 ovoliunlem1 25522 ovoliunlem2 25523 ovolicc2lem1 25537 ovolicc2lem2 25538 ovolicc2lem3 25539 ovolicc2lem4 25540 ovolicc2lem5 25541 dyadmbl 25620 fsumvma 27242 opreu2reuALT 32405 disjxpin 32508 2ndimaxp 32564 2ndresdju 32566 fsumiunle 32730 gsummpt2d 32917 erler 33120 rlocaddval 33123 rlocmulval 33124 cnre2csqima 33726 tpr2rico 33727 esum2dlem 33925 esumiun 33927 1stmbfm 34094 dya2iocnrect 34115 sibfof 34174 sitgaddlemb 34182 hgt750lemb 34502 satefvfmla0 35246 mvrsfpw 35334 msubff 35358 msubco 35359 msubvrs 35388 elxp8 37078 finixpnum 37306 poimirlem4 37325 poimirlem5 37326 poimirlem6 37327 poimirlem7 37328 poimirlem8 37329 poimirlem9 37330 poimirlem10 37331 poimirlem11 37332 poimirlem12 37333 poimirlem13 37334 poimirlem14 37335 poimirlem15 37336 poimirlem16 37337 poimirlem17 37338 poimirlem18 37339 poimirlem19 37340 poimirlem20 37341 poimirlem21 37342 poimirlem22 37343 poimirlem25 37346 poimirlem26 37347 poimirlem27 37348 poimirlem29 37350 poimirlem31 37352 heicant 37356 mblfinlem1 37358 mblfinlem2 37359 ftc2nc 37403 heiborlem8 37519 dvhfvadd 40790 dvhvaddcl 40794 dvhvaddcomN 40795 dvhvaddass 40796 dvhvscacl 40802 dvhgrp 40806 dvhlveclem 40807 dibelval2nd 40851 dicelval2nd 40888 aks6d1c2p1 41816 aks6d1c3 41821 aks6d1c4 41822 aks6d1c6lem2 41869 aks6d1c6lem4 41871 f1o2d2 41957 rmxypairf1o 42569 frmy 42572 cnmetcoval 44809 dvnprodlem1 45567 dvnprodlem2 45568 volicoff 45616 voliooicof 45617 etransclem44 45899 etransclem45 45900 etransclem47 45902 hoissre 46165 hoiprodcl 46168 ovnsubaddlem1 46191 ovnhoilem2 46223 hoicoto2 46226 ovncvr2 46232 opnvonmbllem2 46254 ovolval2lem 46264 ovolval3 46268 ovolval4lem1 46270 ovolval4lem2 46271 ovolval5lem2 46274 ovnovollem1 46277 ovnovollem2 46278 smfpimbor1lem1 46419 2arymaptf 48040 rrx2xpref1o 48106 pgindlem 48461

W3C validator

	
		OSZAR »