Theorem 1st2nd 8053

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

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1534   ∈ wcel 2099  Vcvv 3462   ⊆ wss 3947  ⟨cop 4639   × cxp 5680  Rel wrel 5687  ‘cfv 6554  1^st c1st 8001  2^nd c2nd 8002

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433  ax-un 7746

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-opab 5216  df-mpt 5237  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-iota 6506  df-fun 6556  df-fv 6562  df-1st 8003  df-2nd 8004

This theorem is referenced by:  2ndrn  8055  1st2ndbr  8056  funfv1st2nd  8060  funelss  8061  elopabi  8076  cnvf1olem  8124  ordpinq  10986  addassnq  11001  mulassnq  11002  distrnq  11004  mulidnq  11006  recmulnq  11007  ltexnq  11018  fsumcnv  15777  fprodcnv  15985  cofulid  17909  cofurid  17910  idffth  17955  cofull  17956  cofth  17957  ressffth  17960  isnat2  17971  nat1st2nd  17974  homadmcd  18064  catciso  18133  prf1st  18228  prf2nd  18229  1st2ndprf  18230  curfuncf  18263  uncfcurf  18264  curf2ndf  18272  yonffthlem  18307  yoniso  18310  dprd2dlem2  20040  dprd2dlem1  20041  dprd2da  20042  mdetunilem9  22613  2ndcctbss  23450  utop2nei  24246  utop3cls  24247  caubl  25327  wlkop  29565  nvop2  30541  nvvop  30542  nvop  30609  phop  30751  fgreu  32589  1stpreimas  32617  gsumhashmul  32925  cvmliftlem1  35113  heiborlem3  37514  rngoi  37600  drngoi  37652  isdrngo1  37657  iscrngo2  37698