Theorem 1st2nd 8045

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 5673	. . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
2		ssel2 3935	. . 3 ⊢ ((𝐵 ⊆ (V × V) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
3	1, 2	sylanb 593	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
4		1st2nd2 8034	. 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 2146  Vcvv 3458   ⊆ wss 3908  ⟨cop 4600   × cxp 5664  Rel wrel 5671  ‘cfv 6543  1^st c1st 7993  2^nd c2nd 7994

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-iota 6499  df-fun 6545  df-fv 6551  df-1st 7995  df-2nd 7996

This theorem is used by:  2ndrn  8047  1st2ndbr  8048  funfv1st2nd  8052  funelss  8053  elopabi  8068  cnvf1olem  8114  ordpinq  10946  addassnq  10961  mulassnq  10962  distrnq  10964  mulidnq  10966  recmulnq  10967  ltexnq  10978  fsumcnv  15850  fprodcnv  16063  cofulid  17972  cofurid  17973  idffth  18017  cofull  18018  cofth  18019  ressffth  18022  isnat2  18033  nat1st2nd  18036  homadmcd  18124  catciso  18193  prf1st  18285  prf2nd  18286  1st2ndprf  18287  curfuncf  18319  uncfcurf  18320  curf2ndf  18328  yonffthlem  18363  yoniso  18366  dprd2dlem2  20143  dprd2dlem1  20144  dprd2da  20145  mdetunilem9  22814  2ndcctbss  23649  utop2nei  24444  utop3cls  24445  caubl  25504  wlkop  30014  nvop2  30997  nvvop  30998  nvop  31065  phop  31207  fgreu  33053  1stpreimas  33088  gsumhashmul  33418  cvmliftlem1  35798  heiborlem3  38505  rngoi  38591  drngoi  38643  isdrngo1  38648  iscrngo2  38689  tposideq  49707  cic1st2nd  49866  cofu1st2nd  49911  oppfval2  49956  oppfoppc2  49961  idfth  49977  up1st2nd  50004  up1st2ndr  50005  uptrlem2  50030  uptra  50034  uobeqw  50038  uobeq  50039  uptr2a  50041  diag1  50123  fuco11bALT  50157  fuco22nat  50165  fucocolem4  50175  precofvalALT  50187  prcoftposcurfucoa  50203  prcofdiag1  50212  prcofdiag  50213  oppfdiag1  50233  oppfdiag  50235  termcfuncval  50351  diagffth  50357  lmddu  50486