Theorem xp2nd 8003

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 5671	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3459	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3459	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7981	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2848	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 481	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 726	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1953	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 219	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1561  ∃wex 1800   ∈ wcel 2143  ⟨cop 4589   × cxp 5646  ‘cfv 6521  2^nd c2nd 7969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-iota 6477  df-fun 6523  df-fv 6529  df-2nd 7971

This theorem is referenced by:  offval22  8067  mpof1o2d  8105  fimaproj  8115  disjen  9106  xpf1o  9111  xpmapenlem  9116  mapunen  9118  djur  9889  r0weon  9980  infxpenlem  9981  fseqdom  9994  axcc2lem  10404  iunfo  10507  iundom2g  10508  enqbreq2  10889  nqereu  10898  addpqf  10913  mulpqf  10915  adderpqlem  10923  mulerpqlem  10924  addassnq  10927  mulassnq  10928  distrnq  10930  mulidnq  10932  recmulnq  10933  ltsonq  10938  lterpq  10939  ltanq  10940  ltmnq  10941  ltexnq  10944  archnq  10949  elreal2  11101  cnref1o  12996  fsumcom2  15811  fprodcom2  16024  ruclem6  16277  ruclem8  16279  ruclem9  16280  ruclem10  16281  ruclem12  16283  eucalgval  16626  eucalginv  16628  eucalglt  16629  eucalgcvga  16630  eucalg  16631  xpsff1o  17607  comfffval2  17743  comfeq  17748  idfucl  17924  funcpropd  17945  fucpropd  18023  xpccatid  18230  1stfcl  18239  2ndfcl  18240  xpcpropd  18250  hofcl  18301  hofpropd  18309  yonedalem3  18322  lsmhash  19755  gsum2dlem2  20021  dprd2da  20094  evlslem4  22136  mdetunilem9  22687  tx1cn  23676  txdis  23699  txlly  23703  txnlly  23704  txhaus  23714  txkgen  23719  txconn  23756  txhmeo  23870  ptuncnv  23874  ptunhmeo  23875  xkohmeo  23882  utop2nei  24317  utop3cls  24318  imasdsf1olem  24440  cnheiborlem  25023  caubl  25377  caublcls  25378  bcthlem2  25394  bcthlem4  25396  bcthlem5  25397  ovolficcss  25538  ovoliunlem1  25571  ovoliunlem2  25572  ovolicc2lem1  25586  ovolicc2lem2  25587  ovolicc2lem3  25588  ovolicc2lem4  25589  ovolicc2lem5  25590  dyadmbl  25669  fsumvma  27284  opreu2reuALT  32682  disjxpin  32794  2ndimaxp  32854  2ndresdju  32857  fsumiunle  33037  gsummpt2d  33235  gsumwrd2dccatlem  33263  conjga  33356  elrgspnlem2  33430  elrgspnsubrunlem2  33435  erler  33452  rlocaddval  33456  rlocmulval  33457  mplvrpmga  33844  cnre2csqima  34210  tpr2rico  34211  esum2dlem  34391  esumiun  34393  1stmbfm  34559  dya2iocnrect  34580  sibfof  34639  sitgaddlemb  34647  hgt750lemb  34952  satefvfmla0  35773  mvrsfpw  35861  msubff  35885  msubco  35886  msubvrs  35915  elxp8  37870  finixpnum  38109  poimirlem4  38128  poimirlem5  38129  poimirlem6  38130  poimirlem7  38131  poimirlem8  38132  poimirlem9  38133  poimirlem10  38134  poimirlem11  38135  poimirlem12  38136  poimirlem13  38137  poimirlem14  38138  poimirlem15  38139  poimirlem16  38140  poimirlem17  38141  poimirlem18  38142  poimirlem19  38143  poimirlem20  38144  poimirlem21  38145  poimirlem22  38146  poimirlem25  38149  poimirlem26  38150  poimirlem27  38151  poimirlem29  38153  poimirlem31  38155  heicant  38159  mblfinlem1  38161  mblfinlem2  38162  ftc2nc  38206  heiborlem8  38322  dvhfvadd  41720  dvhvaddcl  41724  dvhvaddcomN  41725  dvhvaddass  41726  dvhvscacl  41732  dvhgrp  41736  dvhlveclem  41737  dibelval2nd  41781  dicelval2nd  41818  aks6d1c2p1  42740  aks6d1c3  42745  aks6d1c4  42746  aks6d1c6lem2  42793  aks6d1c6lem4  42795  rmxypairf1o  43493  frmy  43496  cnmetcoval  45770  dvnprodlem1  46511  dvnprodlem2  46512  volicoff  46560  voliooicof  46561  etransclem44  46843  etransclem45  46844  etransclem47  46846  hoissre  47109  hoiprodcl  47112  ovnsubaddlem1  47135  ovnhoilem2  47167  hoicoto2  47170  ovncvr2  47176  opnvonmbllem2  47198  ovolval2lem  47208  ovolval3  47212  ovolval4lem1  47214  ovolval4lem2  47215  ovolval5lem2  47218  ovnovollem1  47221  ovnovollem2  47222  smfpimbor1lem1  47363  2arymaptf  49265  rrx2xpref1o  49331  elxpcbasex2ALT  49863  swapf2f1oa  49889  swapfida  49892  fuco2eld2  49926  fucoco2  49970  pgindlem  50327