MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1st2nd Structured version   Visualization version   GIF version

Theorem 1st2nd 7724
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
StepHypRef Expression
1 df-rel 5530 . . 3 (Rel 𝐵𝐵 ⊆ (V × V))
2 ssel2 3913 . . 3 ((𝐵 ⊆ (V × V) ∧ 𝐴𝐵) → 𝐴 ∈ (V × V))
31, 2sylanb 584 . 2 ((Rel 𝐵𝐴𝐵) → 𝐴 ∈ (V × V))
4 1st2nd2 7714 . 2 (𝐴 ∈ (V × V) → 𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)
53, 4syl 17 1 ((Rel 𝐵𝐴𝐵) → 𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2112  Vcvv 3444  wss 3884  cop 4534   × cxp 5521  Rel wrel 5528  cfv 6328  1st c1st 7673  2nd c2nd 7674
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-iota 6287  df-fun 6330  df-fv 6336  df-1st 7675  df-2nd 7676
This theorem is referenced by:  2ndrn  7726  1st2ndbr  7727  funfv1st2nd  7731  funelss  7732  elopabi  7746  cnvf1olem  7792  ordpinq  10358  addassnq  10373  mulassnq  10374  distrnq  10376  mulidnq  10378  recmulnq  10379  ltexnq  10390  fsumcnv  15124  fprodcnv  15333  cofulid  17156  cofurid  17157  idffth  17199  cofull  17200  cofth  17201  ressffth  17204  isnat2  17214  nat1st2nd  17217  homadmcd  17298  catciso  17363  prf1st  17450  prf2nd  17451  1st2ndprf  17452  curfuncf  17484  uncfcurf  17485  curf2ndf  17493  yonffthlem  17528  yoniso  17531  dprd2dlem2  19159  dprd2dlem1  19160  dprd2da  19161  mdetunilem9  21229  2ndcctbss  22064  utop2nei  22860  utop3cls  22861  caubl  23916  wlkop  27421  nvop2  28395  nvvop  28396  nvop  28463  phop  28605  fgreu  30439  1stpreimas  30469  gsumhashmul  30745  cvmliftlem1  32646  heiborlem3  35250  rngoi  35336  drngoi  35388  isdrngo1  35393  iscrngo2  35434
  Copyright terms: Public domain W3C validator