Theorem xp2nd 8005

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 5699	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3479	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3479	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 7983	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2819	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 479	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 715	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1936	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 216	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  ∃wex 1782   ∈ wcel 2107  ⟨cop 4634   × cxp 5674  ‘cfv 6541  2^nd c2nd 7971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6493  df-fun 6543  df-fv 6549  df-2nd 7973

This theorem is referenced by:  offval22  8071  fimaproj  8118  disjen  9131  xpf1o  9136  xpmapenlem  9141  mapunen  9143  djur  9911  r0weon  10004  infxpenlem  10005  fseqdom  10018  axcc2lem  10428  iunfo  10531  iundom2g  10532  enqbreq2  10912  nqereu  10921  addpqf  10936  mulpqf  10938  adderpqlem  10946  mulerpqlem  10947  addassnq  10950  mulassnq  10951  distrnq  10953  mulidnq  10955  recmulnq  10956  ltsonq  10961  lterpq  10962  ltanq  10963  ltmnq  10964  ltexnq  10967  archnq  10972  elreal2  11124  cnref1o  12966  fsumcom2  15717  fprodcom2  15925  ruclem6  16175  ruclem8  16177  ruclem9  16178  ruclem10  16179  ruclem12  16181  eucalgval  16516  eucalginv  16518  eucalglt  16519  eucalgcvga  16520  eucalg  16521  xpsff1o  17510  comfffval2  17642  comfeq  17647  idfucl  17828  funcpropd  17848  fucpropd  17927  xpccatid  18137  1stfcl  18146  2ndfcl  18147  xpcpropd  18158  hofcl  18209  hofpropd  18217  yonedalem3  18230  lsmhash  19568  gsum2dlem2  19834  dprd2da  19907  evlslem4  21629  mdetunilem9  22114  tx1cn  23105  txdis  23128  txlly  23132  txnlly  23133  txhaus  23143  txkgen  23148  txconn  23185  txhmeo  23299  ptuncnv  23303  ptunhmeo  23304  xkohmeo  23311  utop2nei  23747  utop3cls  23748  imasdsf1olem  23871  cnheiborlem  24462  caubl  24817  caublcls  24818  bcthlem2  24834  bcthlem4  24836  bcthlem5  24837  ovolficcss  24978  ovoliunlem1  25011  ovoliunlem2  25012  ovolicc2lem1  25026  ovolicc2lem2  25027  ovolicc2lem3  25028  ovolicc2lem4  25029  ovolicc2lem5  25030  dyadmbl  25109  fsumvma  26706  opreu2reuALT  31705  disjxpin  31807  2ndimaxp  31860  2ndresdju  31862  fsumiunle  32023  gsummpt2d  32189  cnre2csqima  32880  tpr2rico  32881  esum2dlem  33079  esumiun  33081  1stmbfm  33248  dya2iocnrect  33269  sibfof  33328  sitgaddlemb  33336  hgt750lemb  33657  satefvfmla0  34398  mvrsfpw  34486  msubff  34510  msubco  34511  msubvrs  34540  elxp8  36241  finixpnum  36462  poimirlem4  36481  poimirlem5  36482  poimirlem6  36483  poimirlem7  36484  poimirlem8  36485  poimirlem9  36486  poimirlem10  36487  poimirlem11  36488  poimirlem12  36489  poimirlem13  36490  poimirlem14  36491  poimirlem15  36492  poimirlem16  36493  poimirlem17  36494  poimirlem18  36495  poimirlem19  36496  poimirlem20  36497  poimirlem21  36498  poimirlem22  36499  poimirlem25  36502  poimirlem26  36503  poimirlem27  36504  poimirlem29  36506  poimirlem31  36508  heicant  36512  mblfinlem1  36514  mblfinlem2  36515  ftc2nc  36559  heiborlem8  36675  dvhfvadd  39951  dvhvaddcl  39955  dvhvaddcomN  39956  dvhvaddass  39957  dvhvscacl  39963  dvhgrp  39967  dvhlveclem  39968  dibelval2nd  40012  dicelval2nd  40049  aks6d1c2p1  40945  f1o2d2  41053  rmxypairf1o  41636  frmy  41639  cnmetcoval  43887  dvnprodlem1  44649  dvnprodlem2  44650  volicoff  44698  voliooicof  44699  etransclem44  44981  etransclem45  44982  etransclem47  44984  hoissre  45247  hoiprodcl  45250  ovnsubaddlem1  45273  ovnhoilem2  45305  hoicoto2  45308  ovncvr2  45314  opnvonmbllem2  45336  ovolval2lem  45346  ovolval3  45350  ovolval4lem1  45352  ovolval4lem2  45353  ovolval5lem2  45356  ovnovollem1  45359  ovnovollem2  45360  smfpimbor1lem1  45501  2arymaptf  47292  rrx2xpref1o  47358  pgindlem  47714