Theorem 1st2nd 8064

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951  ⟨cop 4632   × cxp 5683  Rel wrel 5690  ‘cfv 6561  1^st c1st 8012  2^nd c2nd 8013

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-iota 6514  df-fun 6563  df-fv 6569  df-1st 8014  df-2nd 8015

This theorem is referenced by:  2ndrn  8066  1st2ndbr  8067  funfv1st2nd  8071  funelss  8072  elopabi  8087  cnvf1olem  8135  ordpinq  10983  addassnq  10998  mulassnq  10999  distrnq  11001  mulidnq  11003  recmulnq  11004  ltexnq  11015  fsumcnv  15809  fprodcnv  16019  cofulid  17935  cofurid  17936  idffth  17980  cofull  17981  cofth  17982  ressffth  17985  isnat2  17996  nat1st2nd  17999  homadmcd  18087  catciso  18156  prf1st  18249  prf2nd  18250  1st2ndprf  18251  curfuncf  18283  uncfcurf  18284  curf2ndf  18292  yonffthlem  18327  yoniso  18330  dprd2dlem2  20060  dprd2dlem1  20061  dprd2da  20062  mdetunilem9  22626  2ndcctbss  23463  utop2nei  24259  utop3cls  24260  caubl  25342  wlkop  29646  nvop2  30627  nvvop  30628  nvop  30695  phop  30837  fgreu  32682  1stpreimas  32715  gsumhashmul  33064  cvmliftlem1  35290  heiborlem3  37820  rngoi  37906  drngoi  37958  isdrngo1  37963  iscrngo2  38004  tposideq  48788  diag1  49004  fuco11bALT  49033  fuco22nat  49041  fucocolem4  49051  precofvalALT  49063