Theorem xp2nd 7199

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 5131	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3203	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3203	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7179	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2686	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 502	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 752	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1860	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 207	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1483  ∃wex 1704   ∈ wcel 1990  ⟨cop 4183   × cxp 5112  ‘cfv 5888  2^nd c2nd 7167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fv 5896  df-2nd 7169

This theorem is referenced by:  offval22  7253  disjen  8117  xpf1o  8122  xpmapenlem  8127  mapunen  8129  r0weon  8835  infxpenlem  8836  fseqdom  8849  axcc2lem  9258  iunfo  9361  iundom2g  9362  enqbreq2  9742  nqereu  9751  addpqf  9766  mulpqf  9768  adderpqlem  9776  mulerpqlem  9777  addassnq  9780  mulassnq  9781  distrnq  9783  mulidnq  9785  recmulnq  9786  ltsonq  9791  lterpq  9792  ltanq  9793  ltmnq  9794  ltexnq  9797  archnq  9802  elreal2  9953  cnref1o  11827  fsumcom2  14505  fsumcom2OLD  14506  fprodcom2  14714  fprodcom2OLD  14715  ruclem6  14964  ruclem8  14966  ruclem9  14967  ruclem10  14968  ruclem12  14970  eucalgval  15295  eucalginv  15297  eucalglt  15298  eucalgcvga  15299  eucalg  15300  xpsff1o  16228  comfffval2  16361  comfeq  16366  idfucl  16541  funcpropd  16560  fucpropd  16637  xpccatid  16828  1stfcl  16837  2ndfcl  16838  xpcpropd  16848  hofcl  16899  hofpropd  16907  yonedalem3  16920  lsmhash  18118  gsum2dlem2  18370  dprd2da  18441  evlslem4  19508  mdetunilem9  20426  tx1cn  21412  txdis  21435  txlly  21439  txnlly  21440  txhaus  21450  txkgen  21455  txconn  21492  txhmeo  21606  ptuncnv  21610  ptunhmeo  21611  xkohmeo  21618  utop2nei  22054  utop3cls  22055  imasdsf1olem  22178  cnheiborlem  22753  caubl  23106  caublcls  23107  bcthlem2  23122  bcthlem4  23124  bcthlem5  23125  ovolficcss  23238  ovoliunlem1  23270  ovoliunlem2  23271  ovolicc2lem1  23285  ovolicc2lem2  23286  ovolicc2lem3  23287  ovolicc2lem4  23288  ovolicc2lem5  23289  dyadmbl  23368  fsumvma  24938  disjxpin  29401  fsumiunle  29575  gsummpt2d  29781  fimaproj  29900  cnre2csqima  29957  tpr2rico  29958  esum2dlem  30154  esumiun  30156  1stmbfm  30322  dya2iocnrect  30343  sibfof  30402  sitgaddlemb  30410  hgt750lemb  30734  mvrsfpw  31403  msubff  31427  msubco  31428  msubvrs  31457  elxp8  33219  finixpnum  33394  poimirlem4  33413  poimirlem5  33414  poimirlem6  33415  poimirlem7  33416  poimirlem8  33417  poimirlem9  33418  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem16  33425  poimirlem17  33426  poimirlem18  33427  poimirlem19  33428  poimirlem20  33429  poimirlem21  33430  poimirlem22  33431  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem29  33438  poimirlem31  33440  heicant  33444  mblfinlem1  33446  mblfinlem2  33447  ftc2nc  33494  heiborlem8  33617  dvhfvadd  36380  dvhvaddcl  36384  dvhvaddcomN  36385  dvhvaddass  36386  dvhvscacl  36392  dvhgrp  36396  dvhlveclem  36397  dibelval2nd  36441  dicelval2nd  36478  rmxypairf1o  37476  frmy  37479  cnmetcoval  39394  dvnprodlem1  40161  dvnprodlem2  40162  volicoff  40212  voliooicof  40213  etransclem44  40495  etransclem45  40496  etransclem47  40498  hoissre  40758  hoiprodcl  40761  ovnsubaddlem1  40784  ovnhoilem2  40816  hoicoto2  40819  ovncvr2  40825  opnvonmbllem2  40847  ovolval2lem  40857  ovolval3  40861  ovolval4lem1  40863  ovolval4lem2  40864  ovolval5lem2  40867  ovnovollem1  40870  ovnovollem2  40871  smfpimbor1lem1  41005