Theorem 1st2nd 7981

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3438   ⊆ wss 3905  ⟨cop 4585   × cxp 5621  Rel wrel 5628  ‘cfv 6486  1^st c1st 7929  2^nd c2nd 7930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-iota 6442  df-fun 6488  df-fv 6494  df-1st 7931  df-2nd 7932

This theorem is referenced by:  2ndrn  7983  1st2ndbr  7984  funfv1st2nd  7988  funelss  7989  elopabi  8004  cnvf1olem  8050  ordpinq  10856  addassnq  10871  mulassnq  10872  distrnq  10874  mulidnq  10876  recmulnq  10877  ltexnq  10888  fsumcnv  15698  fprodcnv  15908  cofulid  17815  cofurid  17816  idffth  17860  cofull  17861  cofth  17862  ressffth  17865  isnat2  17876  nat1st2nd  17879  homadmcd  17967  catciso  18036  prf1st  18128  prf2nd  18129  1st2ndprf  18130  curfuncf  18162  uncfcurf  18163  curf2ndf  18171  yonffthlem  18206  yoniso  18209  dprd2dlem2  19939  dprd2dlem1  19940  dprd2da  19941  mdetunilem9  22523  2ndcctbss  23358  utop2nei  24154  utop3cls  24155  caubl  25224  wlkop  29591  nvop2  30570  nvvop  30571  nvop  30638  phop  30780  fgreu  32629  1stpreimas  32662  gsumhashmul  33027  cvmliftlem1  35257  heiborlem3  37792  rngoi  37878  drngoi  37930  isdrngo1  37935  iscrngo2  37976  tposideq  48873  cic1st2nd  49033  cofu1st2nd  49078  oppfval2  49123  oppfoppc2  49128  idfth  49144  up1st2nd  49171  up1st2ndr  49172  uptrlem2  49197  uptra  49201  uobeqw  49205  uobeq  49206  uptr2a  49208  diag1  49290  fuco11bALT  49324  fuco22nat  49332  fucocolem4  49342  precofvalALT  49354  prcoftposcurfucoa  49370  prcofdiag1  49379  prcofdiag  49380  oppfdiag1  49400  oppfdiag  49402  termcfuncval  49518  diagffth  49524  lmddu  49653