Theorem 1st2nd 8032

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  Vcvv 3455   ⊆ wss 3905  ⟨cop 4595   × cxp 5659  Rel wrel 5666  ‘cfv 6536  1^st c1st 7980  2^nd c2nd 7981

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-iota 6492  df-fun 6538  df-fv 6544  df-1st 7982  df-2nd 7983

This theorem is used by:  2ndrn  8034  1st2ndbr  8035  funfv1st2nd  8039  funelss  8040  elopabi  8055  cnvf1olem  8101  ordpinq  10932  addassnq  10947  mulassnq  10948  distrnq  10950  mulidnq  10952  recmulnq  10953  ltexnq  10964  fsumcnv  15829  fprodcnv  16042  cofulid  17951  cofurid  17952  idffth  17996  cofull  17997  cofth  17998  ressffth  18001  isnat2  18012  nat1st2nd  18015  homadmcd  18103  catciso  18172  prf1st  18264  prf2nd  18265  1st2ndprf  18266  curfuncf  18298  uncfcurf  18299  curf2ndf  18307  yonffthlem  18342  yoniso  18345  dprd2dlem2  20116  dprd2dlem1  20117  dprd2da  20118  mdetunilem9  22786  2ndcctbss  23621  utop2nei  24416  utop3cls  24417  caubl  25476  wlkop  29986  nvop2  30969  nvvop  30970  nvop  31037  phop  31179  fgreu  33025  1stpreimas  33060  gsumhashmul  33396  cvmliftlem1  35785  heiborlem3  38492  rngoi  38578  drngoi  38630  isdrngo1  38635  iscrngo2  38676  tposideq  49694  cic1st2nd  49853  cofu1st2nd  49898  oppfval2  49943  oppfoppc2  49948  idfth  49964  up1st2nd  49991  up1st2ndr  49992  uptrlem2  50017  uptra  50021  uobeqw  50025  uobeq  50026  uptr2a  50028  diag1  50110  fuco11bALT  50144  fuco22nat  50152  fucocolem4  50162  precofvalALT  50174  prcoftposcurfucoa  50190  prcofdiag1  50199  prcofdiag  50200  oppfdiag1  50220  oppfdiag  50222  termcfuncval  50338  diagffth  50344  lmddu  50473