Theorem xp2nd 8017

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ⟨cop 4589   × cxp 5645  ‘cfv 6527  2^nd c2nd 7983

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7734

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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-iota 6483  df-fun 6529  df-fv 6535  df-2nd 7985

This theorem is used by:  offval22  8082  mpof1o2d  8120  fimaproj  8130  disjen  9131  xpf1o  9136  xpmapenlem  9141  mapunen  9143  djur  9971  r0weon  10062  infxpenlem  10063  fseqdom  10076  axcc2lem  10485  iunfo  10594  iundom2g  10595  enqbreq2  10976  nqereu  10985  addpqf  11000  mulpqf  11002  adderpqlem  11010  mulerpqlem  11011  addassnq  11014  mulassnq  11015  distrnq  11017  mulidnq  11019  recmulnq  11020  ltsonq  11025  lterpq  11026  ltanq  11027  ltmnq  11028  ltexnq  11031  archnq  11036  elreal2  11188  cnref1o  13082  fsumcom2  15907  fprodcom2  16118  ruclem6  16370  ruclem8  16372  ruclem9  16373  ruclem10  16374  ruclem12  16376  eucalgval  16719  eucalginv  16721  eucalglt  16722  eucalgcvga  16723  eucalg  16724  xpsff1o  17700  comfffval2  17836  comfeq  17841  idfucl  18017  funcpropd  18038  fucpropd  18116  xpccatid  18323  1stfcl  18332  2ndfcl  18333  xpcpropd  18343  hofcl  18394  hofpropd  18402  yonedalem3  18415  lsmhash  19880  gsum2dlem2  20146  dprd2da  20219  evlslem4  22346  mdetunilem9  22896  tx1cn  23889  txdis  23912  txlly  23916  txnlly  23917  txhaus  23927  txkgen  23932  txconn  23969  txhmeo  24083  ptuncnv  24087  ptunhmeo  24088  xkohmeo  24095  utop2nei  24530  utop3cls  24531  imasdsf1olem  24653  cnheiborlem  25236  caubl  25590  caublcls  25591  bcthlem2  25607  bcthlem4  25609  bcthlem5  25610  ovolficcss  25751  ovoliunlem1  25784  ovoliunlem2  25785  ovolicc2lem1  25799  ovolicc2lem2  25800  ovolicc2lem3  25801  ovolicc2lem4  25802  ovolicc2lem5  25803  dyadmbl  25882  fsumvma  27503  opreu2reuALT  33006  disjxpin  33115  2ndimaxp  33173  2ndresdju  33176  fsumiunle  33353  gsummpt2d  33543  gsumwrd2dccatlem  33571  conjga  33664  elrgspnlem2  33737  elrgspnsubrunlem2  33742  erler  33759  rlocaddval  33763  rlocmulval  33764  mplvrpmga  34110  cnre2csqima  34476  tpr2rico  34477  esum2dlem  34657  esumiun  34659  1stmbfm  34826  dya2iocnrect  34847  sibfof  34906  sitgaddlemb  34914  hgt750lemb  35219  satefvfmla0  36104  mvrsfpw  36192  msubff  36216  msubco  36217  msubvrs  36246  elxp8  38214  finixpnum  38448  poimirlem4  38462  poimirlem5  38463  poimirlem6  38464  poimirlem7  38465  poimirlem8  38466  poimirlem9  38467  poimirlem10  38468  poimirlem11  38469  poimirlem12  38470  poimirlem13  38471  poimirlem14  38472  poimirlem15  38473  poimirlem16  38474  poimirlem17  38475  poimirlem18  38476  poimirlem19  38477  poimirlem20  38478  poimirlem21  38479  poimirlem22  38480  poimirlem25  38483  poimirlem26  38484  poimirlem27  38485  poimirlem29  38487  poimirlem31  38489  heicant  38493  mblfinlem1  38495  mblfinlem2  38496  ftc2nc  38540  heiborlem8  38672  dvhfvadd  42068  dvhvaddcl  42072  dvhvaddcomN  42073  dvhvaddass  42074  dvhvscacl  42080  dvhgrp  42084  dvhlveclem  42085  dibelval2nd  42129  dicelval2nd  42166  aks6d1c2p1  43088  aks6d1c3  43093  aks6d1c4  43094  aks6d1c6lem2  43141  aks6d1c6lem4  43143  rmxypairf1o  43856  frmy  43859  cnmetcoval  46137  dvnprodlem1  46878  dvnprodlem2  46879  volicoff  46927  voliooicof  46928  etransclem44  47210  etransclem45  47211  etransclem47  47213  hoissre  47476  hoiprodcl  47479  ovnsubaddlem1  47502  ovnhoilem2  47534  hoicoto2  47537  ovncvr2  47543  opnvonmbllem2  47565  ovolval2lem  47575  ovolval3  47579  ovolval4lem1  47581  ovolval4lem2  47582  ovolval5lem2  47585  ovnovollem1  47588  ovnovollem2  47589  smfpimbor1lem1  47730  2arymaptf  49686  rrx2xpref1o  49752  elxpcbasex2ALT  50281  swapf2f1oa  50307  swapfida  50310  fuco2eld2  50344  fucoco2  50388  pgindlem  50730