Theorem xp2nd 8058

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 5678	. 2 ⊢ (𝐴 ∈ (𝐵 × 𝐶) ↔ ∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
2		vex 3458	. . . . . . 7 ⊢ 𝑏 ∈ V
3		vex 3458	. . . . . . 7 ⊢ 𝑐 ∈ V
4	2, 3	op2ndd 8036	. . . . . 6 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → (2nd ‘𝐴) = 𝑐)
5	4	eleq1d 2849	. . . . 5 ⊢ (𝐴 = ⟨𝑏, 𝑐⟩ → ((2nd ‘𝐴) ∈ 𝐶 ↔ 𝑐 ∈ 𝐶))
6	5	biimpar 483	. . . 4 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ 𝑐 ∈ 𝐶) → (2nd ‘𝐴) ∈ 𝐶)
7	6	adantrl 729	. . 3 ⊢ ((𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
8	7	exlimivv 1967	. 2 ⊢ (∃𝑏∃𝑐(𝐴 = ⟨𝑏, 𝑐⟩ ∧ (𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) → (2nd ‘𝐴) ∈ 𝐶)
9	1, 8	sylbi 220	1 ⊢ (𝐴 ∈ (𝐵 × 𝐶) → (2nd ‘𝐴) ∈ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ⟨cop 4838   × cxp 5653  ‘cfv 6558  2^nd c2nd 8024

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fv 6566  df-2nd 8026

This theorem is used by:  offval22  8124  mpof1o2d  8164  fimaproj  8179  disjen  9181  xpf1o  9186  xpmapenlem  9191  mapunen  9193  djur  10027  r0weon  10118  infxpenlem  10119  fseqdom  10132  axcc2lem  10541  iunfo  10650  iundom2g  10651  enqbreq2  11032  nqereu  11041  addpqf  11056  mulpqf  11058  adderpqlem  11066  mulerpqlem  11067  addassnq  11070  mulassnq  11071  distrnq  11073  mulidnq  11075  recmulnq  11076  ltsonq  11081  lterpq  11082  ltanq  11083  ltmnq  11084  ltexnq  11087  archnq  11092  elreal2  11244  cnref1o  13140  fsumcom2  15969  fprodcom2  16180  ruclem6  16432  ruclem8  16434  ruclem9  16435  ruclem10  16436  ruclem12  16438  eucalgval  16786  eucalginv  16788  eucalglt  16789  eucalgcvga  16790  eucalg  16791  xpsff1o  17768  comfffval2  17904  comfeq  17909  idfucl  18085  funcpropd  18106  fucpropd  18184  xpccatid  18391  1stfcl  18400  2ndfcl  18401  xpcpropd  18411  hofcl  18462  hofpropd  18470  yonedalem3  18483  lsmhash  19949  gsum2dlem2  20215  dprd2da  20288  evlslem4  22415  mdetunilem9  22965  tx1cn  23958  txdis  23981  txlly  23985  txnlly  23986  txhaus  23996  txkgen  24001  txconn  24038  txhmeo  24152  ptuncnv  24156  ptunhmeo  24157  xkohmeo  24164  utop2nei  24599  utop3cls  24600  imasdsf1olem  24722  cnheiborlem  25305  caubl  25659  caublcls  25660  bcthlem2  25676  bcthlem4  25678  bcthlem5  25679  ovolficcss  25820  ovoliunlem1  25853  ovoliunlem2  25854  ovolicc2lem1  25868  ovolicc2lem2  25869  ovolicc2lem3  25870  ovolicc2lem4  25871  ovolicc2lem5  25872  dyadmbl  25951  fsumvma  27570  opreu2reuALT  33145  disjxpin  33254  2ndimaxp  33312  2ndresdju  33315  fsumiunle  33490  gsummpt2d  33680  gsumwrd2dccatlem  33708  conjga  33801  elrgspnlem2  33874  elrgspnsubrunlem2  33879  erler  33896  rlocaddval  33900  rlocmulval  33901  mplvrpmga  34247  cnre2csqima  34613  tpr2rico  34614  esum2dlem  34794  esumiun  34796  1stmbfm  34962  dya2iocnrect  34983  sibfof  35042  sitgaddlemb  35050  hgt750lemb  35355  jf1  36010  dfk12  36012  dfk22  36013  dfk32  36014  k2on  36016  k39o  36017  satefvfmla0  36350  mvrsfpw  36438  msubff  36462  msubco  36463  msubvrs  36492  elxp8  38486  finixpnum  38720  poimirlem4  38734  poimirlem5  38735  poimirlem6  38736  poimirlem7  38737  poimirlem8  38738  poimirlem9  38739  poimirlem10  38740  poimirlem11  38741  poimirlem12  38742  poimirlem13  38743  poimirlem14  38744  poimirlem15  38745  poimirlem16  38746  poimirlem17  38747  poimirlem18  38748  poimirlem19  38749  poimirlem20  38750  poimirlem21  38751  poimirlem22  38752  poimirlem25  38755  poimirlem26  38756  poimirlem27  38757  poimirlem29  38759  poimirlem31  38761  heicant  38765  mblfinlem1  38767  mblfinlem2  38768  ftc2nc  38812  heiborlem8  38944  dvhfvadd  42340  dvhvaddcl  42344  dvhvaddcomN  42345  dvhvaddass  42346  dvhvscacl  42352  dvhgrp  42356  dvhlveclem  42357  dibelval2nd  42401  dicelval2nd  42438  aks6d1c2p1  43360  aks6d1c3  43365  aks6d1c4  43366  aks6d1c6lem2  43413  aks6d1c6lem4  43415  rmxypairf1o  44111  frmy  44114  cnmetcoval  46421  dvnprodlem1  47161  dvnprodlem2  47162  volicoff  47210  voliooicof  47211  etransclem44  47493  etransclem45  47494  etransclem47  47496  hoissre  47759  hoiprodcl  47762  ovnsubaddlem1  47785  ovnhoilem2  47817  hoicoto2  47820  ovncvr2  47826  opnvonmbllem2  47848  ovolval2lem  47858  ovolval3  47862  ovolval4lem1  47864  ovolval4lem2  47865  ovolval5lem2  47868  ovnovollem1  47871  ovnovollem2  47872  smfpimbor1lem1  48013  2arymaptf  49969  elxpcbasex2ALT  50578  swapf2f1oa  50604  swapfida  50607  fuco2eld2  50641  fucoco2  50685  pgindlem  51088