Theorem 1st2nd 7853

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  Vcvv 3422   ⊆ wss 3883  ⟨cop 4564   × cxp 5578  Rel wrel 5585  ‘cfv 6418  1^st c1st 7802  2^nd c2nd 7803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fv 6426  df-1st 7804  df-2nd 7805

This theorem is referenced by:  2ndrn  7855  1st2ndbr  7856  funfv1st2nd  7860  funelss  7861  elopabi  7875  cnvf1olem  7921  ordpinq  10630  addassnq  10645  mulassnq  10646  distrnq  10648  mulidnq  10650  recmulnq  10651  ltexnq  10662  fsumcnv  15413  fprodcnv  15621  cofulid  17521  cofurid  17522  idffth  17565  cofull  17566  cofth  17567  ressffth  17570  isnat2  17580  nat1st2nd  17583  homadmcd  17673  catciso  17742  prf1st  17837  prf2nd  17838  1st2ndprf  17839  curfuncf  17872  uncfcurf  17873  curf2ndf  17881  yonffthlem  17916  yoniso  17919  dprd2dlem2  19558  dprd2dlem1  19559  dprd2da  19560  mdetunilem9  21677  2ndcctbss  22514  utop2nei  23310  utop3cls  23311  caubl  24377  wlkop  27897  nvop2  28871  nvvop  28872  nvop  28939  phop  29081  fgreu  30911  1stpreimas  30940  gsumhashmul  31218  cvmliftlem1  33147  heiborlem3  35898  rngoi  35984  drngoi  36036  isdrngo1  36041  iscrngo2  36082