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

Theorem 1st2nd 7199
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 5111 . . 3 (Rel 𝐵𝐵 ⊆ (V × V))
2 ssel2 3590 . . 3 ((𝐵 ⊆ (V × V) ∧ 𝐴𝐵) → 𝐴 ∈ (V × V))
31, 2sylanb 489 . 2 ((Rel 𝐵𝐴𝐵) → 𝐴 ∈ (V × V))
4 1st2nd2 7190 . 2 (𝐴 ∈ (V × V) → 𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)
53, 4syl 17 1 ((Rel 𝐵𝐴𝐵) → 𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1481  wcel 1988  Vcvv 3195  wss 3567  cop 4174   × cxp 5102  Rel wrel 5109  cfv 5876  1st c1st 7151  2nd c2nd 7152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-iota 5839  df-fun 5878  df-fv 5884  df-1st 7153  df-2nd 7154
This theorem is referenced by:  2ndrn  7201  1st2ndbr  7202  elopabi  7216  cnvf1olem  7260  ordpinq  9750  addassnq  9765  mulassnq  9766  distrnq  9768  mulidnq  9770  recmulnq  9771  ltexnq  9782  fsumcnv  14485  fprodcnv  14694  cofulid  16531  cofurid  16532  idffth  16574  cofull  16575  cofth  16576  ressffth  16579  isnat2  16589  nat1st2nd  16592  homadmcd  16673  catciso  16738  prf1st  16825  prf2nd  16826  1st2ndprf  16827  curfuncf  16859  uncfcurf  16860  curf2ndf  16868  yonffthlem  16903  yoniso  16906  dprd2dlem2  18420  dprd2dlem1  18421  dprd2da  18422  mdetunilem9  20407  2ndcctbss  21239  utop2nei  22035  utop3cls  22036  caubl  23087  wlkop  26504  nvop2  27433  nvvop  27434  nvop  27501  phop  27643  fgreu  29445  1stpreimas  29457  cvmliftlem1  31241  heiborlem3  33583  rngoi  33669  drngoi  33721  isdrngo1  33726  iscrngo2  33767
  Copyright terms: Public domain W3C validator