Theorem xp2nd 8034

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ⟨cop 4589   × cxp 5648  ‘cfv 6538  2^nd c2nd 8000

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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-ss 3896  df-dif 4047  df-in 4091  df-un 4151  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 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6540  df-fv 6546  df-2nd 8002

This theorem is used by:  offval22  8099  mpof1o2d  8137  fimaproj  8152  disjen  9153  xpf1o  9158  xpmapenlem  9163  mapunen  9165  djur  10000  r0weon  10091  infxpenlem  10092  fseqdom  10105  axcc2lem  10514  iunfo  10623  iundom2g  10624  enqbreq2  11005  nqereu  11014  addpqf  11029  mulpqf  11031  adderpqlem  11039  mulerpqlem  11040  addassnq  11043  mulassnq  11044  distrnq  11046  mulidnq  11048  recmulnq  11049  ltsonq  11054  lterpq  11055  ltanq  11056  ltmnq  11057  ltexnq  11060  archnq  11065  elreal2  11217  cnref1o  13113  fsumcom2  15940  fprodcom2  16151  ruclem6  16403  ruclem8  16405  ruclem9  16406  ruclem10  16407  ruclem12  16409  eucalgval  16757  eucalginv  16759  eucalglt  16760  eucalgcvga  16761  eucalg  16762  xpsff1o  17739  comfffval2  17875  comfeq  17880  idfucl  18056  funcpropd  18077  fucpropd  18155  xpccatid  18362  1stfcl  18371  2ndfcl  18372  xpcpropd  18382  hofcl  18433  hofpropd  18441  yonedalem3  18454  lsmhash  19919  gsum2dlem2  20185  dprd2da  20258  evlslem4  22385  mdetunilem9  22935  tx1cn  23928  txdis  23951  txlly  23955  txnlly  23956  txhaus  23966  txkgen  23971  txconn  24008  txhmeo  24122  ptuncnv  24126  ptunhmeo  24127  xkohmeo  24134  utop2nei  24569  utop3cls  24570  imasdsf1olem  24692  cnheiborlem  25275  caubl  25629  caublcls  25630  bcthlem2  25646  bcthlem4  25648  bcthlem5  25649  ovolficcss  25790  ovoliunlem1  25823  ovoliunlem2  25824  ovolicc2lem1  25838  ovolicc2lem2  25839  ovolicc2lem3  25840  ovolicc2lem4  25841  ovolicc2lem5  25842  dyadmbl  25921  fsumvma  27540  opreu2reuALT  33115  disjxpin  33224  2ndimaxp  33282  2ndresdju  33285  fsumiunle  33462  gsummpt2d  33652  gsumwrd2dccatlem  33680  conjga  33773  elrgspnlem2  33846  elrgspnsubrunlem2  33851  erler  33868  rlocaddval  33872  rlocmulval  33873  mplvrpmga  34219  cnre2csqima  34585  tpr2rico  34586  esum2dlem  34766  esumiun  34768  1stmbfm  34934  dya2iocnrect  34955  sibfof  35014  sitgaddlemb  35022  hgt750lemb  35327  satefvfmla0  36225  mvrsfpw  36313  msubff  36337  msubco  36338  msubvrs  36367  elxp8  38337  finixpnum  38571  poimirlem4  38585  poimirlem5  38586  poimirlem6  38587  poimirlem7  38588  poimirlem8  38589  poimirlem9  38590  poimirlem10  38591  poimirlem11  38592  poimirlem12  38593  poimirlem13  38594  poimirlem14  38595  poimirlem15  38596  poimirlem16  38597  poimirlem17  38598  poimirlem18  38599  poimirlem19  38600  poimirlem20  38601  poimirlem21  38602  poimirlem22  38603  poimirlem25  38606  poimirlem26  38607  poimirlem27  38608  poimirlem29  38610  poimirlem31  38612  heicant  38616  mblfinlem1  38618  mblfinlem2  38619  ftc2nc  38663  heiborlem8  38795  dvhfvadd  42191  dvhvaddcl  42195  dvhvaddcomN  42196  dvhvaddass  42197  dvhvscacl  42203  dvhgrp  42207  dvhlveclem  42208  dibelval2nd  42252  dicelval2nd  42289  aks6d1c2p1  43211  aks6d1c3  43216  aks6d1c4  43217  aks6d1c6lem2  43264  aks6d1c6lem4  43266  rmxypairf1o  43961  frmy  43964  cnmetcoval  46259  dvnprodlem1  46999  dvnprodlem2  47000  volicoff  47048  voliooicof  47049  etransclem44  47331  etransclem45  47332  etransclem47  47334  hoissre  47597  hoiprodcl  47600  ovnsubaddlem1  47623  ovnhoilem2  47655  hoicoto2  47658  ovncvr2  47664  opnvonmbllem2  47686  ovolval2lem  47696  ovolval3  47700  ovolval4lem1  47702  ovolval4lem2  47703  ovolval5lem2  47706  ovnovollem1  47709  ovnovollem2  47710  smfpimbor1lem1  47851  2arymaptf  49807  rrx2xpref1o  49873  elxpcbasex2ALT  50402  swapf2f1oa  50428  swapfida  50431  fuco2eld2  50465  fucoco2  50509  pgindlem  50851