Theorem 1st2nd 7993

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 5639	. . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
2		ssel2 3930	. . 3 ⊢ ((𝐵 ⊆ (V × V) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
3	1, 2	sylanb 582	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
4		1st2nd2 7982	. 2 ⊢ (𝐴 ∈ (V × V) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
5	3, 4	syl 17	1 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903  ⟨cop 4588   × cxp 5630  Rel wrel 5637  ‘cfv 6500  1^st c1st 7941  2^nd c2nd 7942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fv 6508  df-1st 7943  df-2nd 7944

This theorem is referenced by:  2ndrn  7995  1st2ndbr  7996  funfv1st2nd  8000  funelss  8001  elopabi  8016  cnvf1olem  8062  ordpinq  10866  addassnq  10881  mulassnq  10882  distrnq  10884  mulidnq  10886  recmulnq  10887  ltexnq  10898  fsumcnv  15708  fprodcnv  15918  cofulid  17826  cofurid  17827  idffth  17871  cofull  17872  cofth  17873  ressffth  17876  isnat2  17887  nat1st2nd  17890  homadmcd  17978  catciso  18047  prf1st  18139  prf2nd  18140  1st2ndprf  18141  curfuncf  18173  uncfcurf  18174  curf2ndf  18182  yonffthlem  18217  yoniso  18220  dprd2dlem2  19983  dprd2dlem1  19984  dprd2da  19985  mdetunilem9  22576  2ndcctbss  23411  utop2nei  24206  utop3cls  24207  caubl  25276  wlkop  29713  nvop2  30695  nvvop  30696  nvop  30763  phop  30905  fgreu  32760  1stpreimas  32795  gsumhashmul  33160  cvmliftlem1  35498  heiborlem3  38058  rngoi  38144  drngoi  38196  isdrngo1  38201  iscrngo2  38242  tposideq  49241  cic1st2nd  49400  cofu1st2nd  49445  oppfval2  49490  oppfoppc2  49495  idfth  49511  up1st2nd  49538  up1st2ndr  49539  uptrlem2  49564  uptra  49568  uobeqw  49572  uobeq  49573  uptr2a  49575  diag1  49657  fuco11bALT  49691  fuco22nat  49699  fucocolem4  49709  precofvalALT  49721  prcoftposcurfucoa  49737  prcofdiag1  49746  prcofdiag  49747  oppfdiag1  49767  oppfdiag  49769  termcfuncval  49885  diagffth  49891  lmddu  50020