Theorem 1st2nd 7988

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  Vcvv 3432   ⊆ wss 3890  ⟨cop 4568   × cxp 5623  Rel wrel 5630  ‘cfv 6492  1^st c1st 7936  2^nd c2nd 7937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fv 6500  df-1st 7938  df-2nd 7939

This theorem is referenced by:  2ndrn  7990  1st2ndbr  7991  funfv1st2nd  7995  funelss  7996  elopabi  8011  cnvf1olem  8056  ordpinq  10864  addassnq  10879  mulassnq  10880  distrnq  10882  mulidnq  10884  recmulnq  10885  ltexnq  10896  fsumcnv  15733  fprodcnv  15946  cofulid  17855  cofurid  17856  idffth  17900  cofull  17901  cofth  17902  ressffth  17905  isnat2  17916  nat1st2nd  17919  homadmcd  18007  catciso  18076  prf1st  18168  prf2nd  18169  1st2ndprf  18170  curfuncf  18202  uncfcurf  18203  curf2ndf  18211  yonffthlem  18246  yoniso  18249  dprd2dlem2  20015  dprd2dlem1  20016  dprd2da  20017  mdetunilem9  22610  2ndcctbss  23445  utop2nei  24240  utop3cls  24241  caubl  25300  wlkop  29721  nvop2  30704  nvvop  30705  nvop  30772  phop  30914  fgreu  32770  1stpreimas  32805  gsumhashmul  33155  cvmliftlem1  35520  heiborlem3  38187  rngoi  38273  drngoi  38325  isdrngo1  38330  iscrngo2  38371  tposideq  49385  cic1st2nd  49544  cofu1st2nd  49589  oppfval2  49634  oppfoppc2  49639  idfth  49655  up1st2nd  49682  up1st2ndr  49683  uptrlem2  49708  uptra  49712  uobeqw  49716  uobeq  49717  uptr2a  49719  diag1  49801  fuco11bALT  49835  fuco22nat  49843  fucocolem4  49853  precofvalALT  49865  prcoftposcurfucoa  49881  prcofdiag1  49890  prcofdiag  49891  oppfdiag1  49911  oppfdiag  49913  termcfuncval  50029  diagffth  50035  lmddu  50164