Theorem 1st2nd 8039

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  Vcvv 3451   ⊆ wss 3899  ⟨cop 4590   × cxp 5649  Rel wrel 5656  ‘cfv 6531  1^st c1st 7988  2^nd c2nd 7989

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fv 6539  df-1st 7990  df-2nd 7991

This theorem is used by:  2ndrn  8041  1st2ndbr  8042  funfv1st2nd  8046  funelss  8047  elopabi  8062  cnvf1olem  8110  ordpinq  11009  addassnq  11024  mulassnq  11025  distrnq  11027  mulidnq  11029  recmulnq  11030  ltexnq  11041  fsumcnv  15919  fprodcnv  16130  cofulid  18045  cofurid  18046  idffth  18090  cofull  18091  cofth  18092  ressffth  18095  isnat2  18106  nat1st2nd  18109  homadmcd  18197  catciso  18266  prf1st  18358  prf2nd  18359  1st2ndprf  18360  curfuncf  18392  uncfcurf  18393  curf2ndf  18401  yonffthlem  18436  yoniso  18439  dprd2dlem2  20236  dprd2dlem1  20237  dprd2da  20238  mdetunilem9  22915  2ndcctbss  23754  utop2nei  24549  utop3cls  24550  caubl  25609  wlkop  30190  nvop2  31192  nvvop  31193  nvop  31260  phop  31402  fgreu  33247  1stpreimas  33281  gsumhashmul  33610  cvmliftlem1  36019  heiborlem3  38715  rngoi  38801  drngoi  38853  isdrngo1  38858  iscrngo2  38899  tposideq  49940  cic1st2nd  50099  cofu1st2nd  50144  oppfval2  50189  oppfoppc2  50194  idfth  50210  up1st2nd  50237  up1st2ndr  50238  uptrlem2  50263  uptra  50267  uobeqw  50271  uobeq  50272  uptr2a  50274  diag1  50356  fuco11bALT  50390  fuco22nat  50398  fucocolem4  50408  precofvalALT  50420  prcoftposcurfucoa  50436  prcofdiag1  50445  prcofdiag  50446  oppfdiag1  50466  oppfdiag  50468  termcfuncval  50584  diagffth  50590  lmddu  50719