Theorem xp2nd 8001

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 5661	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3451	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3451	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7979	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2813	. . . . 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 4595   × cxp 5636  ‘cfv 6511  2^nd c2nd 7967

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fv 6519  df-2nd 7969

This theorem is referenced by:  offval22  8067  fimaproj  8114  disjen  9098  xpf1o  9103  xpmapenlem  9108  mapunen  9110  djur  9872  r0weon  9965  infxpenlem  9966  fseqdom  9979  axcc2lem  10389  iunfo  10492  iundom2g  10493  enqbreq2  10873  nqereu  10882  addpqf  10897  mulpqf  10899  adderpqlem  10907  mulerpqlem  10908  addassnq  10911  mulassnq  10912  distrnq  10914  mulidnq  10916  recmulnq  10917  ltsonq  10922  lterpq  10923  ltanq  10924  ltmnq  10925  ltexnq  10928  archnq  10933  elreal2  11085  cnref1o  12944  fsumcom2  15740  fprodcom2  15950  ruclem6  16203  ruclem8  16205  ruclem9  16206  ruclem10  16207  ruclem12  16209  eucalgval  16552  eucalginv  16554  eucalglt  16555  eucalgcvga  16556  eucalg  16557  xpsff1o  17530  comfffval2  17662  comfeq  17667  idfucl  17843  funcpropd  17864  fucpropd  17942  xpccatid  18149  1stfcl  18158  2ndfcl  18159  xpcpropd  18169  hofcl  18220  hofpropd  18228  yonedalem3  18241  lsmhash  19635  gsum2dlem2  19901  dprd2da  19974  evlslem4  21983  mdetunilem9  22507  tx1cn  23496  txdis  23519  txlly  23523  txnlly  23524  txhaus  23534  txkgen  23539  txconn  23576  txhmeo  23690  ptuncnv  23694  ptunhmeo  23695  xkohmeo  23702  utop2nei  24138  utop3cls  24139  imasdsf1olem  24261  cnheiborlem  24853  caubl  25208  caublcls  25209  bcthlem2  25225  bcthlem4  25227  bcthlem5  25228  ovolficcss  25370  ovoliunlem1  25403  ovoliunlem2  25404  ovolicc2lem1  25418  ovolicc2lem2  25419  ovolicc2lem3  25420  ovolicc2lem4  25421  ovolicc2lem5  25422  dyadmbl  25501  fsumvma  27124  opreu2reuALT  32406  disjxpin  32517  2ndimaxp  32570  2ndresdju  32573  fsumiunle  32754  gsummpt2d  32989  gsumwrd2dccatlem  33006  conjga  33127  elrgspnlem2  33194  elrgspnsubrunlem2  33199  erler  33216  rlocaddval  33219  rlocmulval  33220  cnre2csqima  33901  tpr2rico  33902  esum2dlem  34082  esumiun  34084  1stmbfm  34251  dya2iocnrect  34272  sibfof  34331  sitgaddlemb  34339  hgt750lemb  34647  satefvfmla0  35405  mvrsfpw  35493  msubff  35517  msubco  35518  msubvrs  35547  elxp8  37359  finixpnum  37599  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem9  37623  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem29  37643  poimirlem31  37645  heicant  37649  mblfinlem1  37651  mblfinlem2  37652  ftc2nc  37696  heiborlem8  37812  dvhfvadd  41085  dvhvaddcl  41089  dvhvaddcomN  41090  dvhvaddass  41091  dvhvscacl  41097  dvhgrp  41101  dvhlveclem  41102  dibelval2nd  41146  dicelval2nd  41183  aks6d1c2p1  42106  aks6d1c3  42111  aks6d1c4  42112  aks6d1c6lem2  42159  aks6d1c6lem4  42161  f1o2d2  42221  rmxypairf1o  42900  frmy  42903  cnmetcoval  45196  dvnprodlem1  45944  dvnprodlem2  45945  volicoff  45993  voliooicof  45994  etransclem44  46276  etransclem45  46277  etransclem47  46279  hoissre  46542  hoiprodcl  46545  ovnsubaddlem1  46568  ovnhoilem2  46600  hoicoto2  46603  ovncvr2  46609  opnvonmbllem2  46631  ovolval2lem  46641  ovolval3  46645  ovolval4lem1  46647  ovolval4lem2  46648  ovolval5lem2  46651  ovnovollem1  46654  ovnovollem2  46655  smfpimbor1lem1  46796  2arymaptf  48641  rrx2xpref1o  48707  elxpcbasex2ALT  49240  swapf2f1oa  49266  swapfida  49269  fuco2eld2  49303  fucoco2  49347  pgindlem  49704