Theorem xp2nd 8020

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 5695	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3473	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3473	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7998	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2813	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 477	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 715	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1928	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534  ∃wex 1774   ∈ wcel 2099  ⟨cop 4630   × cxp 5670  ‘cfv 6542  2^nd c2nd 7986

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 2164  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-mpt 5226  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-iota 6494  df-fun 6544  df-fv 6550  df-2nd 7988

This theorem is referenced by:  offval22  8087  fimaproj  8134  disjen  9150  xpf1o  9155  xpmapenlem  9160  mapunen  9162  djur  9934  r0weon  10027  infxpenlem  10028  fseqdom  10041  axcc2lem  10451  iunfo  10554  iundom2g  10555  enqbreq2  10935  nqereu  10944  addpqf  10959  mulpqf  10961  adderpqlem  10969  mulerpqlem  10970  addassnq  10973  mulassnq  10974  distrnq  10976  mulidnq  10978  recmulnq  10979  ltsonq  10984  lterpq  10985  ltanq  10986  ltmnq  10987  ltexnq  10990  archnq  10995  elreal2  11147  cnref1o  12991  fsumcom2  15744  fprodcom2  15952  ruclem6  16203  ruclem8  16205  ruclem9  16206  ruclem10  16207  ruclem12  16209  eucalgval  16544  eucalginv  16546  eucalglt  16547  eucalgcvga  16548  eucalg  16549  xpsff1o  17540  comfffval2  17672  comfeq  17677  idfucl  17858  funcpropd  17880  fucpropd  17960  xpccatid  18170  1stfcl  18179  2ndfcl  18180  xpcpropd  18191  hofcl  18242  hofpropd  18250  yonedalem3  18263  lsmhash  19651  gsum2dlem2  19917  dprd2da  19990  evlslem4  22007  mdetunilem9  22509  tx1cn  23500  txdis  23523  txlly  23527  txnlly  23528  txhaus  23538  txkgen  23543  txconn  23580  txhmeo  23694  ptuncnv  23698  ptunhmeo  23699  xkohmeo  23706  utop2nei  24142  utop3cls  24143  imasdsf1olem  24266  cnheiborlem  24867  caubl  25223  caublcls  25224  bcthlem2  25240  bcthlem4  25242  bcthlem5  25243  ovolficcss  25385  ovoliunlem1  25418  ovoliunlem2  25419  ovolicc2lem1  25433  ovolicc2lem2  25434  ovolicc2lem3  25435  ovolicc2lem4  25436  ovolicc2lem5  25437  dyadmbl  25516  fsumvma  27133  opreu2reuALT  32261  disjxpin  32363  2ndimaxp  32416  2ndresdju  32418  fsumiunle  32574  gsummpt2d  32741  cnre2csqima  33448  tpr2rico  33449  esum2dlem  33647  esumiun  33649  1stmbfm  33816  dya2iocnrect  33837  sibfof  33896  sitgaddlemb  33904  hgt750lemb  34224  satefvfmla0  34964  mvrsfpw  35052  msubff  35076  msubco  35077  msubvrs  35106  elxp8  36786  finixpnum  37013  poimirlem4  37032  poimirlem5  37033  poimirlem6  37034  poimirlem7  37035  poimirlem8  37036  poimirlem9  37037  poimirlem10  37038  poimirlem11  37039  poimirlem12  37040  poimirlem13  37041  poimirlem14  37042  poimirlem15  37043  poimirlem16  37044  poimirlem17  37045  poimirlem18  37046  poimirlem19  37047  poimirlem20  37048  poimirlem21  37049  poimirlem22  37050  poimirlem25  37053  poimirlem26  37054  poimirlem27  37055  poimirlem29  37057  poimirlem31  37059  heicant  37063  mblfinlem1  37065  mblfinlem2  37066  ftc2nc  37110  heiborlem8  37226  dvhfvadd  40501  dvhvaddcl  40505  dvhvaddcomN  40506  dvhvaddass  40507  dvhvscacl  40513  dvhgrp  40517  dvhlveclem  40518  dibelval2nd  40562  dicelval2nd  40599  aks6d1c2p1  41522  aks6d1c3  41527  aks6d1c6lem2  41575  f1o2d2  41644  rmxypairf1o  42254  frmy  42257  cnmetcoval  44498  dvnprodlem1  45257  dvnprodlem2  45258  volicoff  45306  voliooicof  45307  etransclem44  45589  etransclem45  45590  etransclem47  45592  hoissre  45855  hoiprodcl  45858  ovnsubaddlem1  45881  ovnhoilem2  45913  hoicoto2  45916  ovncvr2  45922  opnvonmbllem2  45944  ovolval2lem  45954  ovolval3  45958  ovolval4lem1  45960  ovolval4lem2  45961  ovolval5lem2  45964  ovnovollem1  45967  ovnovollem2  45968  smfpimbor1lem1  46109  2arymaptf  47648  rrx2xpref1o  47714  pgindlem  48069