Theorem xp2nd 8047

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 5708	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3484	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3484	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 8025	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2826	. . . . 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 4632   × cxp 5683  ‘cfv 6561  2^nd c2nd 8013

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fv 6569  df-2nd 8015

This theorem is referenced by:  offval22  8113  fimaproj  8160  disjen  9174  xpf1o  9179  xpmapenlem  9184  mapunen  9186  djur  9959  r0weon  10052  infxpenlem  10053  fseqdom  10066  axcc2lem  10476  iunfo  10579  iundom2g  10580  enqbreq2  10960  nqereu  10969  addpqf  10984  mulpqf  10986  adderpqlem  10994  mulerpqlem  10995  addassnq  10998  mulassnq  10999  distrnq  11001  mulidnq  11003  recmulnq  11004  ltsonq  11009  lterpq  11010  ltanq  11011  ltmnq  11012  ltexnq  11015  archnq  11020  elreal2  11172  cnref1o  13027  fsumcom2  15810  fprodcom2  16020  ruclem6  16271  ruclem8  16273  ruclem9  16274  ruclem10  16275  ruclem12  16277  eucalgval  16619  eucalginv  16621  eucalglt  16622  eucalgcvga  16623  eucalg  16624  xpsff1o  17612  comfffval2  17744  comfeq  17749  idfucl  17926  funcpropd  17947  fucpropd  18025  xpccatid  18233  1stfcl  18242  2ndfcl  18243  xpcpropd  18253  hofcl  18304  hofpropd  18312  yonedalem3  18325  lsmhash  19723  gsum2dlem2  19989  dprd2da  20062  evlslem4  22100  mdetunilem9  22626  tx1cn  23617  txdis  23640  txlly  23644  txnlly  23645  txhaus  23655  txkgen  23660  txconn  23697  txhmeo  23811  ptuncnv  23815  ptunhmeo  23816  xkohmeo  23823  utop2nei  24259  utop3cls  24260  imasdsf1olem  24383  cnheiborlem  24986  caubl  25342  caublcls  25343  bcthlem2  25359  bcthlem4  25361  bcthlem5  25362  ovolficcss  25504  ovoliunlem1  25537  ovoliunlem2  25538  ovolicc2lem1  25552  ovolicc2lem2  25553  ovolicc2lem3  25554  ovolicc2lem4  25555  ovolicc2lem5  25556  dyadmbl  25635  fsumvma  27257  opreu2reuALT  32496  disjxpin  32601  2ndimaxp  32656  2ndresdju  32659  fsumiunle  32831  gsummpt2d  33052  gsumwrd2dccatlem  33069  elrgspnlem2  33247  elrgspnsubrunlem2  33252  erler  33269  rlocaddval  33272  rlocmulval  33273  cnre2csqima  33910  tpr2rico  33911  esum2dlem  34093  esumiun  34095  1stmbfm  34262  dya2iocnrect  34283  sibfof  34342  sitgaddlemb  34350  hgt750lemb  34671  satefvfmla0  35423  mvrsfpw  35511  msubff  35535  msubco  35536  msubvrs  35565  elxp8  37372  finixpnum  37612  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem9  37636  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem14  37641  poimirlem15  37642  poimirlem16  37643  poimirlem17  37644  poimirlem18  37645  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem29  37656  poimirlem31  37658  heicant  37662  mblfinlem1  37664  mblfinlem2  37665  ftc2nc  37709  heiborlem8  37825  dvhfvadd  41093  dvhvaddcl  41097  dvhvaddcomN  41098  dvhvaddass  41099  dvhvscacl  41105  dvhgrp  41109  dvhlveclem  41110  dibelval2nd  41154  dicelval2nd  41191  aks6d1c2p1  42119  aks6d1c3  42124  aks6d1c4  42125  aks6d1c6lem2  42172  aks6d1c6lem4  42174  f1o2d2  42274  rmxypairf1o  42923  frmy  42926  cnmetcoval  45207  dvnprodlem1  45961  dvnprodlem2  45962  volicoff  46010  voliooicof  46011  etransclem44  46293  etransclem45  46294  etransclem47  46296  hoissre  46559  hoiprodcl  46562  ovnsubaddlem1  46585  ovnhoilem2  46617  hoicoto2  46620  ovncvr2  46626  opnvonmbllem2  46648  ovolval2lem  46658  ovolval3  46662  ovolval4lem1  46664  ovolval4lem2  46665  ovolval5lem2  46668  ovnovollem1  46671  ovnovollem2  46672  smfpimbor1lem1  46813  2arymaptf  48573  rrx2xpref1o  48639  elxpcbasex2ALT  48957  swapf2f1oa  48983  swapfida  48986  fuco2eld2  49009  fucoco2  49053  pgindlem  49234