Theorem 1st2nd 8024

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 5658	. . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
2		ssel2 3934	. . 3 ⊢ ((𝐵 ⊆ (V × V) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
3	1, 2	sylanb 592	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
4		1st2nd2 8013	. 2 ⊢ (𝐴 ∈ (V × V) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
5	3, 4	syl 18	1 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  Vcvv 3457   ⊆ wss 3907  ⟨cop 4591   × cxp 5649  Rel wrel 5656  ‘cfv 6525  1^st c1st 7972  2^nd c2nd 7973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6481  df-fun 6527  df-fv 6533  df-1st 7974  df-2nd 7975

This theorem is referenced by:  2ndrn  8026  1st2ndbr  8027  funfv1st2nd  8031  funelss  8032  elopabi  8047  cnvf1olem  8093  ordpinq  10916  addassnq  10931  mulassnq  10932  distrnq  10934  mulidnq  10936  recmulnq  10937  ltexnq  10948  fsumcnv  15812  fprodcnv  16025  cofulid  17935  cofurid  17936  idffth  17980  cofull  17981  cofth  17982  ressffth  17985  isnat2  17996  nat1st2nd  17999  homadmcd  18087  catciso  18156  prf1st  18248  prf2nd  18249  1st2ndprf  18250  curfuncf  18282  uncfcurf  18283  curf2ndf  18291  yonffthlem  18326  yoniso  18329  dprd2dlem2  20100  dprd2dlem1  20101  dprd2da  20102  mdetunilem9  22734  2ndcctbss  23569  utop2nei  24364  utop3cls  24365  caubl  25424  wlkop  29882  nvop2  30865  nvvop  30866  nvop  30933  phop  31075  fgreu  32924  1stpreimas  32959  gsumhashmul  33295  cvmliftlem1  35643  heiborlem3  38319  rngoi  38405  drngoi  38457  isdrngo1  38462  iscrngo2  38503  tposideq  49518  cic1st2nd  49677  cofu1st2nd  49722  oppfval2  49767  oppfoppc2  49772  idfth  49788  up1st2nd  49815  up1st2ndr  49816  uptrlem2  49841  uptra  49845  uobeqw  49849  uobeq  49850  uptr2a  49852  diag1  49934  fuco11bALT  49968  fuco22nat  49976  fucocolem4  49986  precofvalALT  49998  prcoftposcurfucoa  50014  prcofdiag1  50023  prcofdiag  50024  oppfdiag1  50044  oppfdiag  50046  termcfuncval  50162  diagffth  50168  lmddu  50297