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

Theorem 1st2nd 8053
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 5689 . . 3 (Rel 𝐵𝐵 ⊆ (V × V))
2 ssel2 3974 . . 3 ((𝐵 ⊆ (V × V) ∧ 𝐴𝐵) → 𝐴 ∈ (V × V))
31, 2sylanb 579 . 2 ((Rel 𝐵𝐴𝐵) → 𝐴 ∈ (V × V))
4 1st2nd2 8042 . 2 (𝐴 ∈ (V × V) → 𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)
53, 4syl 17 1 ((Rel 𝐵𝐴𝐵) → 𝐴 = ⟨(1st𝐴), (2nd𝐴)⟩)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1534  wcel 2099  Vcvv 3462  wss 3947  cop 4639   × cxp 5680  Rel wrel 5687  cfv 6554  1st c1st 8001  2nd c2nd 8002
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-iota 6506  df-fun 6556  df-fv 6562  df-1st 8003  df-2nd 8004
This theorem is referenced by:  2ndrn  8055  1st2ndbr  8056  funfv1st2nd  8060  funelss  8061  elopabi  8076  cnvf1olem  8124  ordpinq  10986  addassnq  11001  mulassnq  11002  distrnq  11004  mulidnq  11006  recmulnq  11007  ltexnq  11018  fsumcnv  15777  fprodcnv  15985  cofulid  17909  cofurid  17910  idffth  17955  cofull  17956  cofth  17957  ressffth  17960  isnat2  17971  nat1st2nd  17974  homadmcd  18064  catciso  18133  prf1st  18228  prf2nd  18229  1st2ndprf  18230  curfuncf  18263  uncfcurf  18264  curf2ndf  18272  yonffthlem  18307  yoniso  18310  dprd2dlem2  20040  dprd2dlem1  20041  dprd2da  20042  mdetunilem9  22613  2ndcctbss  23450  utop2nei  24246  utop3cls  24247  caubl  25327  wlkop  29565  nvop2  30541  nvvop  30542  nvop  30609  phop  30751  fgreu  32589  1stpreimas  32617  gsumhashmul  32925  cvmliftlem1  35113  heiborlem3  37514  rngoi  37600  drngoi  37652  isdrngo1  37657  iscrngo2  37698
  Copyright terms: Public domain W3C validator