Theorem 1st2nd 7985

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  ⟨cop 4574   × cxp 5622  Rel wrel 5629  ‘cfv 6492  1^st c1st 7933  2^nd c2nd 7934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-1st 7935  df-2nd 7936

This theorem is referenced by:  2ndrn  7987  1st2ndbr  7988  funfv1st2nd  7992  funelss  7993  elopabi  8008  cnvf1olem  8053  ordpinq  10857  addassnq  10872  mulassnq  10873  distrnq  10875  mulidnq  10877  recmulnq  10878  ltexnq  10889  fsumcnv  15726  fprodcnv  15939  cofulid  17848  cofurid  17849  idffth  17893  cofull  17894  cofth  17895  ressffth  17898  isnat2  17909  nat1st2nd  17912  homadmcd  18000  catciso  18069  prf1st  18161  prf2nd  18162  1st2ndprf  18163  curfuncf  18195  uncfcurf  18196  curf2ndf  18204  yonffthlem  18239  yoniso  18242  dprd2dlem2  20008  dprd2dlem1  20009  dprd2da  20010  mdetunilem9  22595  2ndcctbss  23430  utop2nei  24225  utop3cls  24226  caubl  25285  wlkop  29711  nvop2  30694  nvvop  30695  nvop  30762  phop  30904  fgreu  32759  1stpreimas  32794  gsumhashmul  33143  cvmliftlem1  35483  heiborlem3  38148  rngoi  38234  drngoi  38286  isdrngo1  38291  iscrngo2  38332  tposideq  49375  cic1st2nd  49534  cofu1st2nd  49579  oppfval2  49624  oppfoppc2  49629  idfth  49645  up1st2nd  49672  up1st2ndr  49673  uptrlem2  49698  uptra  49702  uobeqw  49706  uobeq  49707  uptr2a  49709  diag1  49791  fuco11bALT  49825  fuco22nat  49833  fucocolem4  49843  precofvalALT  49855  prcoftposcurfucoa  49871  prcofdiag1  49880  prcofdiag  49881  oppfdiag1  49901  oppfdiag  49903  termcfuncval  50019  diagffth  50025  lmddu  50154