Theorem 1st2nd 7199

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1481   ∈ wcel 1988  Vcvv 3195   ⊆ wss 3567  ⟨cop 4174   × cxp 5102  Rel wrel 5109  ‘cfv 5876  1^st c1st 7151  2^nd c2nd 7152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-sbc 3430  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-iota 5839  df-fun 5878  df-fv 5884  df-1st 7153  df-2nd 7154

This theorem is referenced by:  2ndrn  7201  1st2ndbr  7202  elopabi  7216  cnvf1olem  7260  ordpinq  9750  addassnq  9765  mulassnq  9766  distrnq  9768  mulidnq  9770  recmulnq  9771  ltexnq  9782  fsumcnv  14485  fprodcnv  14694  cofulid  16531  cofurid  16532  idffth  16574  cofull  16575  cofth  16576  ressffth  16579  isnat2  16589  nat1st2nd  16592  homadmcd  16673  catciso  16738  prf1st  16825  prf2nd  16826  1st2ndprf  16827  curfuncf  16859  uncfcurf  16860  curf2ndf  16868  yonffthlem  16903  yoniso  16906  dprd2dlem2  18420  dprd2dlem1  18421  dprd2da  18422  mdetunilem9  20407  2ndcctbss  21239  utop2nei  22035  utop3cls  22036  caubl  23087  wlkop  26504  nvop2  27433  nvvop  27434  nvop  27501  phop  27643  fgreu  29445  1stpreimas  29457  cvmliftlem1  31241  heiborlem3  33583  rngoi  33669  drngoi  33721  isdrngo1  33726  iscrngo2  33767