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 5698	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3478	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3478	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7982	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2818	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 478	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 714	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1935	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106  ⟨cop 4633   × cxp 5673  ‘cfv 6540  2^nd c2nd 7970

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6492  df-fun 6542  df-fv 6548  df-2nd 7972

This theorem is referenced by:  offval22  8070  fimaproj  8117  disjen  9130  xpf1o  9135  xpmapenlem  9140  mapunen  9142  djur  9910  r0weon  10003  infxpenlem  10004  fseqdom  10017  axcc2lem  10427  iunfo  10530  iundom2g  10531  enqbreq2  10911  nqereu  10920  addpqf  10935  mulpqf  10937  adderpqlem  10945  mulerpqlem  10946  addassnq  10949  mulassnq  10950  distrnq  10952  mulidnq  10954  recmulnq  10955  ltsonq  10960  lterpq  10961  ltanq  10962  ltmnq  10963  ltexnq  10966  archnq  10971  elreal2  11123  cnref1o  12965  fsumcom2  15716  fprodcom2  15924  ruclem6  16174  ruclem8  16176  ruclem9  16177  ruclem10  16178  ruclem12  16180  eucalgval  16515  eucalginv  16517  eucalglt  16518  eucalgcvga  16519  eucalg  16520  xpsff1o  17509  comfffval2  17641  comfeq  17646  idfucl  17827  funcpropd  17847  fucpropd  17926  xpccatid  18136  1stfcl  18145  2ndfcl  18146  xpcpropd  18157  hofcl  18208  hofpropd  18216  yonedalem3  18229  lsmhash  19567  gsum2dlem2  19833  dprd2da  19906  evlslem4  21628  mdetunilem9  22113  tx1cn  23104  txdis  23127  txlly  23131  txnlly  23132  txhaus  23142  txkgen  23147  txconn  23184  txhmeo  23298  ptuncnv  23302  ptunhmeo  23303  xkohmeo  23310  utop2nei  23746  utop3cls  23747  imasdsf1olem  23870  cnheiborlem  24461  caubl  24816  caublcls  24817  bcthlem2  24833  bcthlem4  24835  bcthlem5  24836  ovolficcss  24977  ovoliunlem1  25010  ovoliunlem2  25011  ovolicc2lem1  25025  ovolicc2lem2  25026  ovolicc2lem3  25027  ovolicc2lem4  25028  ovolicc2lem5  25029  dyadmbl  25108  fsumvma  26705  opreu2reuALT  31704  disjxpin  31806  2ndimaxp  31859  2ndresdju  31861  fsumiunle  32022  gsummpt2d  32188  cnre2csqima  32879  tpr2rico  32880  esum2dlem  33078  esumiun  33080  1stmbfm  33247  dya2iocnrect  33268  sibfof  33327  sitgaddlemb  33335  hgt750lemb  33656  satefvfmla0  34397  mvrsfpw  34485  msubff  34509  msubco  34510  msubvrs  34539  elxp8  36240  finixpnum  36461  poimirlem4  36480  poimirlem5  36481  poimirlem6  36482  poimirlem7  36483  poimirlem8  36484  poimirlem9  36485  poimirlem10  36486  poimirlem11  36487  poimirlem12  36488  poimirlem13  36489  poimirlem14  36490  poimirlem15  36491  poimirlem16  36492  poimirlem17  36493  poimirlem18  36494  poimirlem19  36495  poimirlem20  36496  poimirlem21  36497  poimirlem22  36498  poimirlem25  36501  poimirlem26  36502  poimirlem27  36503  poimirlem29  36505  poimirlem31  36507  heicant  36511  mblfinlem1  36513  mblfinlem2  36514  ftc2nc  36558  heiborlem8  36674  dvhfvadd  39950  dvhvaddcl  39954  dvhvaddcomN  39955  dvhvaddass  39956  dvhvscacl  39962  dvhgrp  39966  dvhlveclem  39967  dibelval2nd  40011  dicelval2nd  40048  aks6d1c2p1  40944  f1o2d2  41052  rmxypairf1o  41635  frmy  41638  cnmetcoval  43886  dvnprodlem1  44648  dvnprodlem2  44649  volicoff  44697  voliooicof  44698  etransclem44  44980  etransclem45  44981  etransclem47  44983  hoissre  45246  hoiprodcl  45249  ovnsubaddlem1  45272  ovnhoilem2  45304  hoicoto2  45307  ovncvr2  45313  opnvonmbllem2  45335  ovolval2lem  45345  ovolval3  45349  ovolval4lem1  45351  ovolval4lem2  45352  ovolval5lem2  45355  ovnovollem1  45358  ovnovollem2  45359  smfpimbor1lem1  45500  2arymaptf  47291  rrx2xpref1o  47357  pgindlem  47713