Theorem xp2nd 7988

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 5659	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3448	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3448	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7966	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2837	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 480	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 724	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1942	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 219	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1550  ∃wex 1789   ∈ wcel 2132  ⟨cop 4578   × cxp 5634  ‘cfv 6506  2^nd c2nd 7954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pr 5380  ax-un 7703

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-iota 6462  df-fun 6508  df-fv 6514  df-2nd 7956

This theorem is referenced by:  offval22  8051  mpof1o2d  8089  fimaproj  8099  disjen  9091  xpf1o  9096  xpmapenlem  9101  mapunen  9103  djur  9863  r0weon  9954  infxpenlem  9955  fseqdom  9968  axcc2lem  10379  iunfo  10482  iundom2g  10483  enqbreq2  10864  nqereu  10873  addpqf  10888  mulpqf  10890  adderpqlem  10898  mulerpqlem  10899  addassnq  10902  mulassnq  10903  distrnq  10905  mulidnq  10907  recmulnq  10908  ltsonq  10913  lterpq  10914  ltanq  10915  ltmnq  10916  ltexnq  10919  archnq  10924  elreal2  11076  cnref1o  12972  fsumcom2  15773  fprodcom2  15986  ruclem6  16239  ruclem8  16241  ruclem9  16242  ruclem10  16243  ruclem12  16245  eucalgval  16588  eucalginv  16590  eucalglt  16591  eucalgcvga  16592  eucalg  16593  xpsff1o  17569  comfffval2  17705  comfeq  17710  idfucl  17886  funcpropd  17907  fucpropd  17985  xpccatid  18192  1stfcl  18201  2ndfcl  18202  xpcpropd  18212  hofcl  18263  hofpropd  18271  yonedalem3  18284  lsmhash  19717  gsum2dlem2  19983  dprd2da  20056  evlslem4  22098  mdetunilem9  22649  tx1cn  23638  txdis  23661  txlly  23665  txnlly  23666  txhaus  23676  txkgen  23681  txconn  23718  txhmeo  23832  ptuncnv  23836  ptunhmeo  23837  xkohmeo  23844  utop2nei  24279  utop3cls  24280  imasdsf1olem  24402  cnheiborlem  24985  caubl  25339  caublcls  25340  bcthlem2  25356  bcthlem4  25358  bcthlem5  25359  ovolficcss  25500  ovoliunlem1  25533  ovoliunlem2  25534  ovolicc2lem1  25548  ovolicc2lem2  25549  ovolicc2lem3  25550  ovolicc2lem4  25551  ovolicc2lem5  25552  dyadmbl  25631  fsumvma  27243  opreu2reuALT  32613  disjxpin  32726  2ndimaxp  32787  2ndresdju  32790  fsumiunle  32970  gsummpt2d  33179  gsumwrd2dccatlem  33207  conjga  33300  elrgspnlem2  33373  elrgspnsubrunlem2  33378  erler  33395  rlocaddval  33398  rlocmulval  33399  mplvrpmga  33786  cnre2csqima  34152  tpr2rico  34153  esum2dlem  34333  esumiun  34335  1stmbfm  34501  dya2iocnrect  34522  sibfof  34581  sitgaddlemb  34589  hgt750lemb  34897  satefvfmla0  35706  mvrsfpw  35794  msubff  35818  msubco  35819  msubvrs  35848  elxp8  37803  finixpnum  38042  poimirlem4  38061  poimirlem5  38062  poimirlem6  38063  poimirlem7  38064  poimirlem8  38065  poimirlem9  38066  poimirlem10  38067  poimirlem11  38068  poimirlem12  38069  poimirlem13  38070  poimirlem14  38071  poimirlem15  38072  poimirlem16  38073  poimirlem17  38074  poimirlem18  38075  poimirlem19  38076  poimirlem20  38077  poimirlem21  38078  poimirlem22  38079  poimirlem25  38082  poimirlem26  38083  poimirlem27  38084  poimirlem29  38086  poimirlem31  38088  heicant  38092  mblfinlem1  38094  mblfinlem2  38095  ftc2nc  38139  heiborlem8  38255  dvhfvadd  41653  dvhvaddcl  41657  dvhvaddcomN  41658  dvhvaddass  41659  dvhvscacl  41665  dvhgrp  41669  dvhlveclem  41670  dibelval2nd  41714  dicelval2nd  41751  aks6d1c2p1  42673  aks6d1c3  42678  aks6d1c4  42679  aks6d1c6lem2  42726  aks6d1c6lem4  42728  rmxypairf1o  43426  frmy  43429  cnmetcoval  45717  dvnprodlem1  46458  dvnprodlem2  46459  volicoff  46507  voliooicof  46508  etransclem44  46790  etransclem45  46791  etransclem47  46793  hoissre  47056  hoiprodcl  47059  ovnsubaddlem1  47082  ovnhoilem2  47114  hoicoto2  47117  ovncvr2  47123  opnvonmbllem2  47145  ovolval2lem  47155  ovolval3  47159  ovolval4lem1  47161  ovolval4lem2  47162  ovolval5lem2  47165  ovnovollem1  47168  ovnovollem2  47169  smfpimbor1lem1  47310  2arymaptf  49212  rrx2xpref1o  49278  elxpcbasex2ALT  49810  swapf2f1oa  49836  swapfida  49839  fuco2eld2  49873  fucoco2  49917  pgindlem  50274