Theorem xp2nd 7585

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

Assertion

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

Proof of Theorem xp2nd

Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp 5473	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3443	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3443	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7563	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2869	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 478	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 712	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1914	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 218	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1525  ∃wex 1765   ∈ wcel 2083  ⟨cop 4484   × cxp 5448  ‘cfv 6232  2^nd c2nd 7551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-iota 6196  df-fun 6234  df-fv 6240  df-2nd 7553

This theorem is referenced by:  offval22  7646  disjen  8528  xpf1o  8533  xpmapenlem  8538  mapunen  8540  djur  9201  r0weon  9291  infxpenlem  9292  fseqdom  9305  axcc2lem  9711  iunfo  9814  iundom2g  9815  enqbreq2  10195  nqereu  10204  addpqf  10219  mulpqf  10221  adderpqlem  10229  mulerpqlem  10230  addassnq  10233  mulassnq  10234  distrnq  10236  mulidnq  10238  recmulnq  10239  ltsonq  10244  lterpq  10245  ltanq  10246  ltmnq  10247  ltexnq  10250  archnq  10255  elreal2  10407  cnref1o  12238  fsumcom2  14966  fprodcom2  15175  ruclem6  15425  ruclem8  15427  ruclem9  15428  ruclem10  15429  ruclem12  15431  eucalgval  15759  eucalginv  15761  eucalglt  15762  eucalgcvga  15763  eucalg  15764  xpsff1o  16673  comfffval2  16804  comfeq  16809  idfucl  16984  funcpropd  17003  fucpropd  17080  xpccatid  17271  1stfcl  17280  2ndfcl  17281  xpcpropd  17291  hofcl  17342  hofpropd  17350  yonedalem3  17363  lsmhash  18562  gsum2dlem2  18815  dprd2da  18885  evlslem4  19979  mdetunilem9  20917  tx1cn  21905  txdis  21928  txlly  21932  txnlly  21933  txhaus  21943  txkgen  21948  txconn  21985  txhmeo  22099  ptuncnv  22103  ptunhmeo  22104  xkohmeo  22111  utop2nei  22546  utop3cls  22547  imasdsf1olem  22670  cnheiborlem  23245  caubl  23598  caublcls  23599  bcthlem2  23615  bcthlem4  23617  bcthlem5  23618  ovolficcss  23757  ovoliunlem1  23790  ovoliunlem2  23791  ovolicc2lem1  23805  ovolicc2lem2  23806  ovolicc2lem3  23807  ovolicc2lem4  23808  ovolicc2lem5  23809  dyadmbl  23888  fsumvma  25475  opreu2reuALT  29928  disjxpin  30024  fsumiunle  30225  gsummpt2d  30492  fimaproj  30710  cnre2csqima  30767  tpr2rico  30768  esum2dlem  30964  esumiun  30966  1stmbfm  31131  dya2iocnrect  31152  sibfof  31211  sitgaddlemb  31219  hgt750lemb  31540  satefvfmla0  32275  mvrsfpw  32363  msubff  32387  msubco  32388  msubvrs  32417  elxp8  34204  finixpnum  34429  poimirlem4  34448  poimirlem5  34449  poimirlem6  34450  poimirlem7  34451  poimirlem8  34452  poimirlem9  34453  poimirlem10  34454  poimirlem11  34455  poimirlem12  34456  poimirlem13  34457  poimirlem14  34458  poimirlem15  34459  poimirlem16  34460  poimirlem17  34461  poimirlem18  34462  poimirlem19  34463  poimirlem20  34464  poimirlem21  34465  poimirlem22  34466  poimirlem25  34469  poimirlem26  34470  poimirlem27  34471  poimirlem29  34473  poimirlem31  34475  heicant  34479  mblfinlem1  34481  mblfinlem2  34482  ftc2nc  34528  heiborlem8  34649  dvhfvadd  37779  dvhvaddcl  37783  dvhvaddcomN  37784  dvhvaddass  37785  dvhvscacl  37791  dvhgrp  37795  dvhlveclem  37796  dibelval2nd  37840  dicelval2nd  37877  rmxypairf1o  39014  frmy  39017  cnmetcoval  41026  dvnprodlem1  41794  dvnprodlem2  41795  volicoff  41844  voliooicof  41845  etransclem44  42127  etransclem45  42128  etransclem47  42130  hoissre  42390  hoiprodcl  42393  ovnsubaddlem1  42416  ovnhoilem2  42448  hoicoto2  42451  ovncvr2  42457  opnvonmbllem2  42479  ovolval2lem  42489  ovolval3  42493  ovolval4lem1  42495  ovolval4lem2  42496  ovolval5lem2  42499  ovnovollem1  42502  ovnovollem2  42503  smfpimbor1lem1  42637  rrx2xpref1o  44208