Theorem xp2nd 8004

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 5664	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3454	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3454	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7982	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2814	. . . . 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 2109  ⟨cop 4598   × cxp 5639  ‘cfv 6514  2^nd c2nd 7970

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fv 6522  df-2nd 7972

This theorem is referenced by:  offval22  8070  fimaproj  8117  disjen  9104  xpf1o  9109  xpmapenlem  9114  mapunen  9116  djur  9879  r0weon  9972  infxpenlem  9973  fseqdom  9986  axcc2lem  10396  iunfo  10499  iundom2g  10500  enqbreq2  10880  nqereu  10889  addpqf  10904  mulpqf  10906  adderpqlem  10914  mulerpqlem  10915  addassnq  10918  mulassnq  10919  distrnq  10921  mulidnq  10923  recmulnq  10924  ltsonq  10929  lterpq  10930  ltanq  10931  ltmnq  10932  ltexnq  10935  archnq  10940  elreal2  11092  cnref1o  12951  fsumcom2  15747  fprodcom2  15957  ruclem6  16210  ruclem8  16212  ruclem9  16213  ruclem10  16214  ruclem12  16216  eucalgval  16559  eucalginv  16561  eucalglt  16562  eucalgcvga  16563  eucalg  16564  xpsff1o  17537  comfffval2  17669  comfeq  17674  idfucl  17850  funcpropd  17871  fucpropd  17949  xpccatid  18156  1stfcl  18165  2ndfcl  18166  xpcpropd  18176  hofcl  18227  hofpropd  18235  yonedalem3  18248  lsmhash  19642  gsum2dlem2  19908  dprd2da  19981  evlslem4  21990  mdetunilem9  22514  tx1cn  23503  txdis  23526  txlly  23530  txnlly  23531  txhaus  23541  txkgen  23546  txconn  23583  txhmeo  23697  ptuncnv  23701  ptunhmeo  23702  xkohmeo  23709  utop2nei  24145  utop3cls  24146  imasdsf1olem  24268  cnheiborlem  24860  caubl  25215  caublcls  25216  bcthlem2  25232  bcthlem4  25234  bcthlem5  25235  ovolficcss  25377  ovoliunlem1  25410  ovoliunlem2  25411  ovolicc2lem1  25425  ovolicc2lem2  25426  ovolicc2lem3  25427  ovolicc2lem4  25428  ovolicc2lem5  25429  dyadmbl  25508  fsumvma  27131  opreu2reuALT  32413  disjxpin  32524  2ndimaxp  32577  2ndresdju  32580  fsumiunle  32761  gsummpt2d  32996  gsumwrd2dccatlem  33013  conjga  33134  elrgspnlem2  33201  elrgspnsubrunlem2  33206  erler  33223  rlocaddval  33226  rlocmulval  33227  cnre2csqima  33908  tpr2rico  33909  esum2dlem  34089  esumiun  34091  1stmbfm  34258  dya2iocnrect  34279  sibfof  34338  sitgaddlemb  34346  hgt750lemb  34654  satefvfmla0  35412  mvrsfpw  35500  msubff  35524  msubco  35525  msubvrs  35554  elxp8  37366  finixpnum  37606  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem8  37629  poimirlem9  37630  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem13  37634  poimirlem14  37635  poimirlem15  37636  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem29  37650  poimirlem31  37652  heicant  37656  mblfinlem1  37658  mblfinlem2  37659  ftc2nc  37703  heiborlem8  37819  dvhfvadd  41092  dvhvaddcl  41096  dvhvaddcomN  41097  dvhvaddass  41098  dvhvscacl  41104  dvhgrp  41108  dvhlveclem  41109  dibelval2nd  41153  dicelval2nd  41190  aks6d1c2p1  42113  aks6d1c3  42118  aks6d1c4  42119  aks6d1c6lem2  42166  aks6d1c6lem4  42168  f1o2d2  42228  rmxypairf1o  42907  frmy  42910  cnmetcoval  45203  dvnprodlem1  45951  dvnprodlem2  45952  volicoff  46000  voliooicof  46001  etransclem44  46283  etransclem45  46284  etransclem47  46286  hoissre  46549  hoiprodcl  46552  ovnsubaddlem1  46575  ovnhoilem2  46607  hoicoto2  46610  ovncvr2  46616  opnvonmbllem2  46638  ovolval2lem  46648  ovolval3  46652  ovolval4lem1  46654  ovolval4lem2  46655  ovolval5lem2  46658  ovnovollem1  46661  ovnovollem2  46662  smfpimbor1lem1  46803  2arymaptf  48645  rrx2xpref1o  48711  elxpcbasex2ALT  49244  swapf2f1oa  49270  swapfida  49273  fuco2eld2  49307  fucoco2  49351  pgindlem  49708