Theorem 1st2nd 7965

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 5620	. . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
2		ssel2 3926	. . 3 ⊢ ((𝐵 ⊆ (V × V) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
3	1, 2	sylanb 581	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
4		1st2nd2 7954	. 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 3433   ⊆ wss 3899  ⟨cop 4579   × cxp 5611  Rel wrel 5618  ‘cfv 6476  1^st c1st 7913  2^nd c2nd 7914

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 2701  ax-sep 5231  ax-nul 5241  ax-pr 5367  ax-un 7662

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3393  df-v 3435  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-opab 5151  df-mpt 5170  df-id 5508  df-xp 5619  df-rel 5620  df-cnv 5621  df-co 5622  df-dm 5623  df-rn 5624  df-iota 6432  df-fun 6478  df-fv 6484  df-1st 7915  df-2nd 7916

This theorem is referenced by:  2ndrn  7967  1st2ndbr  7968  funfv1st2nd  7972  funelss  7973  elopabi  7988  cnvf1olem  8034  ordpinq  10825  addassnq  10840  mulassnq  10841  distrnq  10843  mulidnq  10845  recmulnq  10846  ltexnq  10857  fsumcnv  15667  fprodcnv  15877  cofulid  17784  cofurid  17785  idffth  17829  cofull  17830  cofth  17831  ressffth  17834  isnat2  17845  nat1st2nd  17848  homadmcd  17936  catciso  18005  prf1st  18097  prf2nd  18098  1st2ndprf  18099  curfuncf  18131  uncfcurf  18132  curf2ndf  18140  yonffthlem  18175  yoniso  18178  dprd2dlem2  19908  dprd2dlem1  19909  dprd2da  19910  mdetunilem9  22489  2ndcctbss  23324  utop2nei  24119  utop3cls  24120  caubl  25189  wlkop  29560  nvop2  30539  nvvop  30540  nvop  30607  phop  30749  fgreu  32606  1stpreimas  32639  gsumhashmul  33009  cvmliftlem1  35275  heiborlem3  37810  rngoi  37896  drngoi  37948  isdrngo1  37953  iscrngo2  37994  tposideq  48886  cic1st2nd  49046  cofu1st2nd  49091  oppfval2  49136  oppfoppc2  49141  idfth  49157  up1st2nd  49184  up1st2ndr  49185  uptrlem2  49210  uptra  49214  uobeqw  49218  uobeq  49219  uptr2a  49221  diag1  49303  fuco11bALT  49337  fuco22nat  49345  fucocolem4  49355  precofvalALT  49367  prcoftposcurfucoa  49383  prcofdiag1  49392  prcofdiag  49393  oppfdiag1  49413  oppfdiag  49415  termcfuncval  49531  diagffth  49537  lmddu  49666