Theorem 1st2nd 8016

Description: Reconstruction of a member of a relation in terms of its ordered pair components. (Contributed by NM, 29-Aug-2006.)

Assertion

Ref	Expression
1st2nd	⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)

Proof of Theorem 1st2nd

Step	Hyp	Ref	Expression
1		df-rel 5652	. . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
2		ssel2 3931	. . 3 ⊢ ((𝐵 ⊆ (V × V) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
3	1, 2	sylanb 590	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
4		1st2nd2 8005	. 2 ⊢ (𝐴 ∈ (V × V) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
5	3, 4	syl 17	1 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  Vcvv 3453   ⊆ wss 3904  ⟨cop 4587   × cxp 5643  Rel wrel 5650  ‘cfv 6517  1^st c1st 7964  2^nd c2nd 7965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pr 5389  ax-un 7714

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-iota 6473  df-fun 6519  df-fv 6525  df-1st 7966  df-2nd 7967

This theorem is referenced by:  2ndrn  8018  1st2ndbr  8019  funfv1st2nd  8023  funelss  8024  elopabi  8039  cnvf1olem  8084  ordpinq  10898  addassnq  10913  mulassnq  10914  distrnq  10916  mulidnq  10918  recmulnq  10919  ltexnq  10930  fsumcnv  15783  fprodcnv  15996  cofulid  17906  cofurid  17907  idffth  17951  cofull  17952  cofth  17953  ressffth  17956  isnat2  17967  nat1st2nd  17970  homadmcd  18058  catciso  18127  prf1st  18219  prf2nd  18220  1st2ndprf  18221  curfuncf  18253  uncfcurf  18254  curf2ndf  18262  yonffthlem  18297  yoniso  18300  dprd2dlem2  20065  dprd2dlem1  20066  dprd2da  20067  mdetunilem9  22660  2ndcctbss  23495  utop2nei  24290  utop3cls  24291  caubl  25350  wlkop  29774  nvop2  30757  nvvop  30758  nvop  30825  phop  30967  fgreu  32823  1stpreimas  32858  gsumhashmul  33208  cvmliftlem1  35599  heiborlem3  38276  rngoi  38362  drngoi  38414  isdrngo1  38419  iscrngo2  38460  tposideq  49473  cic1st2nd  49632  cofu1st2nd  49677  oppfval2  49722  oppfoppc2  49727  idfth  49743  up1st2nd  49770  up1st2ndr  49771  uptrlem2  49796  uptra  49800  uobeqw  49804  uobeq  49805  uptr2a  49807  diag1  49889  fuco11bALT  49923  fuco22nat  49931  fucocolem4  49941  precofvalALT  49953  prcoftposcurfucoa  49969  prcofdiag1  49978  prcofdiag  49979  oppfdiag1  49999  oppfdiag  50001  termcfuncval  50117  diagffth  50123  lmddu  50252