Theorem xp2nd 8019

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 5677	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3463	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3463	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7997	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2819	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 477	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 716	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1932	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 217	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ⟨cop 4607   × cxp 5652  ‘cfv 6530  2^nd c2nd 7985

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6483  df-fun 6532  df-fv 6538  df-2nd 7987

This theorem is referenced by:  offval22  8085  fimaproj  8132  disjen  9146  xpf1o  9151  xpmapenlem  9156  mapunen  9158  djur  9931  r0weon  10024  infxpenlem  10025  fseqdom  10038  axcc2lem  10448  iunfo  10551  iundom2g  10552  enqbreq2  10932  nqereu  10941  addpqf  10956  mulpqf  10958  adderpqlem  10966  mulerpqlem  10967  addassnq  10970  mulassnq  10971  distrnq  10973  mulidnq  10975  recmulnq  10976  ltsonq  10981  lterpq  10982  ltanq  10983  ltmnq  10984  ltexnq  10987  archnq  10992  elreal2  11144  cnref1o  12999  fsumcom2  15788  fprodcom2  15998  ruclem6  16251  ruclem8  16253  ruclem9  16254  ruclem10  16255  ruclem12  16257  eucalgval  16599  eucalginv  16601  eucalglt  16602  eucalgcvga  16603  eucalg  16604  xpsff1o  17579  comfffval2  17711  comfeq  17716  idfucl  17892  funcpropd  17913  fucpropd  17991  xpccatid  18198  1stfcl  18207  2ndfcl  18208  xpcpropd  18218  hofcl  18269  hofpropd  18277  yonedalem3  18290  lsmhash  19684  gsum2dlem2  19950  dprd2da  20023  evlslem4  22032  mdetunilem9  22556  tx1cn  23545  txdis  23568  txlly  23572  txnlly  23573  txhaus  23583  txkgen  23588  txconn  23625  txhmeo  23739  ptuncnv  23743  ptunhmeo  23744  xkohmeo  23751  utop2nei  24187  utop3cls  24188  imasdsf1olem  24310  cnheiborlem  24902  caubl  25258  caublcls  25259  bcthlem2  25275  bcthlem4  25277  bcthlem5  25278  ovolficcss  25420  ovoliunlem1  25453  ovoliunlem2  25454  ovolicc2lem1  25468  ovolicc2lem2  25469  ovolicc2lem3  25470  ovolicc2lem4  25471  ovolicc2lem5  25472  dyadmbl  25551  fsumvma  27174  opreu2reuALT  32404  disjxpin  32515  2ndimaxp  32570  2ndresdju  32573  fsumiunle  32754  gsummpt2d  32989  gsumwrd2dccatlem  33006  elrgspnlem2  33184  elrgspnsubrunlem2  33189  erler  33206  rlocaddval  33209  rlocmulval  33210  cnre2csqima  33888  tpr2rico  33889  esum2dlem  34069  esumiun  34071  1stmbfm  34238  dya2iocnrect  34259  sibfof  34318  sitgaddlemb  34326  hgt750lemb  34634  satefvfmla0  35386  mvrsfpw  35474  msubff  35498  msubco  35499  msubvrs  35528  elxp8  37335  finixpnum  37575  poimirlem4  37594  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem9  37599  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem13  37603  poimirlem14  37604  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem29  37619  poimirlem31  37621  heicant  37625  mblfinlem1  37627  mblfinlem2  37628  ftc2nc  37672  heiborlem8  37788  dvhfvadd  41056  dvhvaddcl  41060  dvhvaddcomN  41061  dvhvaddass  41062  dvhvscacl  41068  dvhgrp  41072  dvhlveclem  41073  dibelval2nd  41117  dicelval2nd  41154  aks6d1c2p1  42077  aks6d1c3  42082  aks6d1c4  42083  aks6d1c6lem2  42130  aks6d1c6lem4  42132  f1o2d2  42231  rmxypairf1o  42882  frmy  42885  cnmetcoval  45174  dvnprodlem1  45923  dvnprodlem2  45924  volicoff  45972  voliooicof  45973  etransclem44  46255  etransclem45  46256  etransclem47  46258  hoissre  46521  hoiprodcl  46524  ovnsubaddlem1  46547  ovnhoilem2  46579  hoicoto2  46582  ovncvr2  46588  opnvonmbllem2  46610  ovolval2lem  46620  ovolval3  46624  ovolval4lem1  46626  ovolval4lem2  46627  ovolval5lem2  46630  ovnovollem1  46633  ovnovollem2  46634  smfpimbor1lem1  46775  2arymaptf  48580  rrx2xpref1o  48646  elxpcbasex2ALT  49116  swapf2f1oa  49142  swapfida  49145  fuco2eld2  49173  fucoco2  49217  pgindlem  49527