Theorem xp2nd 7964

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 5643	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3431	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3431	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7942	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2820	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 477	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 717	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1934	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 217	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ⟨cop 4563   × cxp 5618  ‘cfv 6487  2^nd c2nd 7930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pr 5364  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2931  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-iota 6443  df-fun 6489  df-fv 6495  df-2nd 7932

This theorem is referenced by:  offval22  8027  fimaproj  8074  disjen  9061  xpf1o  9066  xpmapenlem  9071  mapunen  9073  djur  9832  r0weon  9923  infxpenlem  9924  fseqdom  9937  axcc2lem  10347  iunfo  10450  iundom2g  10451  enqbreq2  10832  nqereu  10841  addpqf  10856  mulpqf  10858  adderpqlem  10866  mulerpqlem  10867  addassnq  10870  mulassnq  10871  distrnq  10873  mulidnq  10875  recmulnq  10876  ltsonq  10881  lterpq  10882  ltanq  10883  ltmnq  10884  ltexnq  10887  archnq  10892  elreal2  11044  cnref1o  12924  fsumcom2  15725  fprodcom2  15938  ruclem6  16191  ruclem8  16193  ruclem9  16194  ruclem10  16195  ruclem12  16197  eucalgval  16540  eucalginv  16542  eucalglt  16543  eucalgcvga  16544  eucalg  16545  xpsff1o  17520  comfffval2  17656  comfeq  17661  idfucl  17837  funcpropd  17858  fucpropd  17936  xpccatid  18143  1stfcl  18152  2ndfcl  18153  xpcpropd  18163  hofcl  18214  hofpropd  18222  yonedalem3  18235  lsmhash  19669  gsum2dlem2  19935  dprd2da  20008  evlslem4  22043  mdetunilem9  22573  tx1cn  23562  txdis  23585  txlly  23589  txnlly  23590  txhaus  23600  txkgen  23605  txconn  23642  txhmeo  23756  ptuncnv  23760  ptunhmeo  23761  xkohmeo  23768  utop2nei  24203  utop3cls  24204  imasdsf1olem  24326  cnheiborlem  24909  caubl  25263  caublcls  25264  bcthlem2  25280  bcthlem4  25282  bcthlem5  25283  ovolficcss  25424  ovoliunlem1  25457  ovoliunlem2  25458  ovolicc2lem1  25472  ovolicc2lem2  25473  ovolicc2lem3  25474  ovolicc2lem4  25475  ovolicc2lem5  25476  dyadmbl  25555  fsumvma  27164  opreu2reuALT  32534  disjxpin  32646  2ndimaxp  32707  2ndresdju  32710  fsumiunle  32890  gsummpt2d  33098  gsumwrd2dccatlem  33126  conjga  33219  elrgspnlem2  33292  elrgspnsubrunlem2  33297  erler  33314  rlocaddval  33317  rlocmulval  33318  mplvrpmga  33677  cnre2csqima  34043  tpr2rico  34044  esum2dlem  34224  esumiun  34226  1stmbfm  34392  dya2iocnrect  34413  sibfof  34472  sitgaddlemb  34480  hgt750lemb  34788  satefvfmla0  35588  mvrsfpw  35676  msubff  35700  msubco  35701  msubvrs  35730  elxp8  37675  finixpnum  37914  poimirlem4  37933  poimirlem5  37934  poimirlem6  37935  poimirlem7  37936  poimirlem8  37937  poimirlem9  37938  poimirlem10  37939  poimirlem11  37940  poimirlem12  37941  poimirlem13  37942  poimirlem14  37943  poimirlem15  37944  poimirlem16  37945  poimirlem17  37946  poimirlem18  37947  poimirlem19  37948  poimirlem20  37949  poimirlem21  37950  poimirlem22  37951  poimirlem25  37954  poimirlem26  37955  poimirlem27  37956  poimirlem29  37958  poimirlem31  37960  heicant  37964  mblfinlem1  37966  mblfinlem2  37967  ftc2nc  38011  heiborlem8  38127  dvhfvadd  41525  dvhvaddcl  41529  dvhvaddcomN  41530  dvhvaddass  41531  dvhvscacl  41537  dvhgrp  41541  dvhlveclem  41542  dibelval2nd  41586  dicelval2nd  41623  aks6d1c2p1  42545  aks6d1c3  42550  aks6d1c4  42551  aks6d1c6lem2  42598  aks6d1c6lem4  42600  f1o2d2  42662  rmxypairf1o  43327  frmy  43330  cnmetcoval  45619  dvnprodlem1  46362  dvnprodlem2  46363  volicoff  46411  voliooicof  46412  etransclem44  46694  etransclem45  46695  etransclem47  46697  hoissre  46960  hoiprodcl  46963  ovnsubaddlem1  46986  ovnhoilem2  47018  hoicoto2  47021  ovncvr2  47027  opnvonmbllem2  47049  ovolval2lem  47059  ovolval3  47063  ovolval4lem1  47065  ovolval4lem2  47066  ovolval5lem2  47069  ovnovollem1  47072  ovnovollem2  47073  smfpimbor1lem1  47214  2arymaptf  49116  rrx2xpref1o  49182  elxpcbasex2ALT  49714  swapf2f1oa  49740  swapfida  49743  fuco2eld2  49777  fucoco2  49821  pgindlem  50178