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 5659	. . 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 5650  Rel wrel 5657  ‘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 5251  ax-nul 5261  ax-pr 5395  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 4869  df-br 5106  df-opab 5168  df-mpt 5187  df-id 5547  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  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  15814  fprodcnv  16027  cofulid  17937  cofurid  17938  idffth  17982  cofull  17983  cofth  17984  ressffth  17987  isnat2  17998  nat1st2nd  18001  homadmcd  18089  catciso  18158  prf1st  18250  prf2nd  18251  1st2ndprf  18252  curfuncf  18284  uncfcurf  18285  curf2ndf  18293  yonffthlem  18328  yoniso  18331  dprd2dlem2  20103  dprd2dlem1  20104  dprd2da  20105  mdetunilem9  22738  2ndcctbss  23573  utop2nei  24368  utop3cls  24369  caubl  25428  wlkop  29886  nvop2  30869  nvvop  30870  nvop  30937  phop  31079  fgreu  32928  1stpreimas  32963  gsumhashmul  33300  cvmliftlem1  35648  heiborlem3  38324  rngoi  38410  drngoi  38462  isdrngo1  38467  iscrngo2  38508  tposideq  49517  cic1st2nd  49676  cofu1st2nd  49721  oppfval2  49766  oppfoppc2  49771  idfth  49787  up1st2nd  49814  up1st2ndr  49815  uptrlem2  49840  uptra  49844  uobeqw  49848  uobeq  49849  uptr2a  49851  diag1  49933  fuco11bALT  49967  fuco22nat  49975  fucocolem4  49985  precofvalALT  49997  prcoftposcurfucoa  50013  prcofdiag1  50022  prcofdiag  50023  oppfdiag1  50043  oppfdiag  50045  termcfuncval  50161  diagffth  50167  lmddu  50296