Theorem xp2nd 8018

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 5684	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3457	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3457	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7996	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2846	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 482	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 728	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1960	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 220	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1568  ∃wex 1807   ∈ wcel 2141  ⟨cop 4594   × cxp 5659  ‘cfv 6536  2^nd c2nd 7984

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-iota 6492  df-fun 6538  df-fv 6544  df-2nd 7986

This theorem is referenced by:  offval22  8082  mpof1o2d  8120  fimaproj  8130  disjen  9121  xpf1o  9126  xpmapenlem  9131  mapunen  9133  djur  9904  r0weon  9995  infxpenlem  9996  fseqdom  10009  axcc2lem  10419  iunfo  10522  iundom2g  10523  enqbreq2  10904  nqereu  10913  addpqf  10928  mulpqf  10930  adderpqlem  10938  mulerpqlem  10939  addassnq  10942  mulassnq  10943  distrnq  10945  mulidnq  10947  recmulnq  10948  ltsonq  10953  lterpq  10954  ltanq  10955  ltmnq  10956  ltexnq  10959  archnq  10964  elreal2  11116  cnref1o  13008  fsumcom2  15824  fprodcom2  16037  ruclem6  16290  ruclem8  16292  ruclem9  16293  ruclem10  16294  ruclem12  16296  eucalgval  16639  eucalginv  16641  eucalglt  16642  eucalgcvga  16643  eucalg  16644  xpsff1o  17620  comfffval2  17756  comfeq  17761  idfucl  17937  funcpropd  17958  fucpropd  18036  xpccatid  18243  1stfcl  18252  2ndfcl  18253  xpcpropd  18263  hofcl  18314  hofpropd  18322  yonedalem3  18335  lsmhash  19774  gsum2dlem2  20040  dprd2da  20113  evlslem4  22206  mdetunilem9  22756  tx1cn  23745  txdis  23768  txlly  23772  txnlly  23773  txhaus  23783  txkgen  23788  txconn  23825  txhmeo  23939  ptuncnv  23943  ptunhmeo  23944  xkohmeo  23951  utop2nei  24386  utop3cls  24387  imasdsf1olem  24509  cnheiborlem  25092  caubl  25446  caublcls  25447  bcthlem2  25463  bcthlem4  25465  bcthlem5  25466  ovolficcss  25607  ovoliunlem1  25640  ovoliunlem2  25641  ovolicc2lem1  25655  ovolicc2lem2  25656  ovolicc2lem3  25657  ovolicc2lem4  25658  ovolicc2lem5  25659  dyadmbl  25738  fsumvma  27353  opreu2reuALT  32789  disjxpin  32899  2ndimaxp  32957  2ndresdju  32960  fsumiunle  33139  gsummpt2d  33335  gsumwrd2dccatlem  33363  conjga  33456  elrgspnlem2  33529  elrgspnsubrunlem2  33534  erler  33551  rlocaddval  33555  rlocmulval  33556  mplvrpmga  33901  cnre2csqima  34267  tpr2rico  34268  esum2dlem  34448  esumiun  34450  1stmbfm  34616  dya2iocnrect  34637  sibfof  34696  sitgaddlemb  34704  hgt750lemb  35009  satefvfmla0  35864  mvrsfpw  35952  msubff  35976  msubco  35977  msubvrs  36006  elxp8  37961  finixpnum  38200  poimirlem4  38219  poimirlem5  38220  poimirlem6  38221  poimirlem7  38222  poimirlem8  38223  poimirlem9  38224  poimirlem10  38225  poimirlem11  38226  poimirlem12  38227  poimirlem13  38228  poimirlem14  38229  poimirlem15  38230  poimirlem16  38231  poimirlem17  38232  poimirlem18  38233  poimirlem19  38234  poimirlem20  38235  poimirlem21  38236  poimirlem22  38237  poimirlem25  38240  poimirlem26  38241  poimirlem27  38242  poimirlem29  38244  poimirlem31  38246  heicant  38250  mblfinlem1  38252  mblfinlem2  38253  ftc2nc  38297  heiborlem8  38413  dvhfvadd  41811  dvhvaddcl  41815  dvhvaddcomN  41816  dvhvaddass  41817  dvhvscacl  41823  dvhgrp  41827  dvhlveclem  41828  dibelval2nd  41872  dicelval2nd  41909  aks6d1c2p1  42831  aks6d1c3  42836  aks6d1c4  42837  aks6d1c6lem2  42884  aks6d1c6lem4  42886  rmxypairf1o  43586  frmy  43589  cnmetcoval  45867  dvnprodlem1  46608  dvnprodlem2  46609  volicoff  46657  voliooicof  46658  etransclem44  46940  etransclem45  46941  etransclem47  46943  hoissre  47206  hoiprodcl  47209  ovnsubaddlem1  47232  ovnhoilem2  47264  hoicoto2  47267  ovncvr2  47273  opnvonmbllem2  47295  ovolval2lem  47305  ovolval3  47309  ovolval4lem1  47311  ovolval4lem2  47312  ovolval5lem2  47315  ovnovollem1  47318  ovnovollem2  47319  smfpimbor1lem1  47460  2arymaptf  49377  rrx2xpref1o  49443  elxpcbasex2ALT  49974  swapf2f1oa  50000  swapfida  50003  fuco2eld2  50037  fucoco2  50081  pgindlem  50438