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

Theorem 1st2nd 7443
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 5315 . . 3 (Rel 𝐵𝐵 ⊆ (V × V))
2 ssel2 3790 . . 3 ((𝐵 ⊆ (V × V) ∧ 𝐴𝐵) → 𝐴 ∈ (V × V))
31, 2sylanb 572 . 2 ((Rel 𝐵𝐴𝐵) → 𝐴 ∈ (V × V))
4 1st2nd2 7434 . 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 1637  wcel 2158  Vcvv 3390  wss 3766  cop 4373   × cxp 5306  Rel wrel 5313  cfv 6098  1st c1st 7393  2nd c2nd 7394
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ral 3100  df-rex 3101  df-rab 3104  df-v 3392  df-sbc 3631  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4627  df-br 4841  df-opab 4903  df-mpt 4920  df-id 5216  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-iota 6061  df-fun 6100  df-fv 6106  df-1st 7395  df-2nd 7396
This theorem is referenced by:  2ndrn  7445  1st2ndbr  7446  elopabi  7461  cnvf1olem  7506  ordpinq  10047  addassnq  10062  mulassnq  10063  distrnq  10065  mulidnq  10067  recmulnq  10068  ltexnq  10079  fsumcnv  14723  fprodcnv  14930  cofulid  16750  cofurid  16751  idffth  16793  cofull  16794  cofth  16795  ressffth  16798  isnat2  16808  nat1st2nd  16811  homadmcd  16892  catciso  16957  prf1st  17045  prf2nd  17046  1st2ndprf  17047  curfuncf  17079  uncfcurf  17080  curf2ndf  17088  yonffthlem  17123  yoniso  17126  dprd2dlem2  18637  dprd2dlem1  18638  dprd2da  18639  mdetunilem9  20633  2ndcctbss  21468  utop2nei  22263  utop3cls  22264  caubl  23314  wlkop  26747  nvop2  27788  nvvop  27789  nvop  27856  phop  27998  fgreu  29795  1stpreimas  29807  cvmliftlem1  31587  heiborlem3  33920  rngoi  34006  drngoi  34058  isdrngo1  34063  iscrngo2  34104
  Copyright terms: Public domain W3C validator