Theorem 1st2nd 8021

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3917  ⟨cop 4598   × cxp 5639  Rel wrel 5646  ‘cfv 6514  1^st c1st 7969  2^nd c2nd 7970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fv 6522  df-1st 7971  df-2nd 7972

This theorem is referenced by:  2ndrn  8023  1st2ndbr  8024  funfv1st2nd  8028  funelss  8029  elopabi  8044  cnvf1olem  8092  ordpinq  10903  addassnq  10918  mulassnq  10919  distrnq  10921  mulidnq  10923  recmulnq  10924  ltexnq  10935  fsumcnv  15746  fprodcnv  15956  cofulid  17859  cofurid  17860  idffth  17904  cofull  17905  cofth  17906  ressffth  17909  isnat2  17920  nat1st2nd  17923  homadmcd  18011  catciso  18080  prf1st  18172  prf2nd  18173  1st2ndprf  18174  curfuncf  18206  uncfcurf  18207  curf2ndf  18215  yonffthlem  18250  yoniso  18253  dprd2dlem2  19979  dprd2dlem1  19980  dprd2da  19981  mdetunilem9  22514  2ndcctbss  23349  utop2nei  24145  utop3cls  24146  caubl  25215  wlkop  29563  nvop2  30544  nvvop  30545  nvop  30612  phop  30754  fgreu  32603  1stpreimas  32636  gsumhashmul  33008  cvmliftlem1  35279  heiborlem3  37814  rngoi  37900  drngoi  37952  isdrngo1  37957  iscrngo2  37998  tposideq  48880  cic1st2nd  49040  cofu1st2nd  49085  oppfval2  49130  oppfoppc2  49135  idfth  49151  up1st2nd  49178  up1st2ndr  49179  uptrlem2  49204  uptra  49208  uobeqw  49212  uobeq  49213  uptr2a  49215  diag1  49297  fuco11bALT  49331  fuco22nat  49339  fucocolem4  49349  precofvalALT  49361  prcoftposcurfucoa  49377  prcofdiag1  49386  prcofdiag  49387  oppfdiag1  49407  oppfdiag  49409  termcfuncval  49525  diagffth  49531  lmddu  49660