Theorem 1st2nd 7873

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1542   ∈ wcel 2110  Vcvv 3431   ⊆ wss 3892  ⟨cop 4573   × cxp 5588  Rel wrel 5595  ‘cfv 6432  1^st c1st 7822  2^nd c2nd 7823

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 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7582

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-iota 6390  df-fun 6434  df-fv 6440  df-1st 7824  df-2nd 7825

This theorem is referenced by:  2ndrn  7875  1st2ndbr  7876  funfv1st2nd  7880  funelss  7881  elopabi  7895  cnvf1olem  7941  ordpinq  10700  addassnq  10715  mulassnq  10716  distrnq  10718  mulidnq  10720  recmulnq  10721  ltexnq  10732  fsumcnv  15483  fprodcnv  15691  cofulid  17603  cofurid  17604  idffth  17647  cofull  17648  cofth  17649  ressffth  17652  isnat2  17662  nat1st2nd  17665  homadmcd  17755  catciso  17824  prf1st  17919  prf2nd  17920  1st2ndprf  17921  curfuncf  17954  uncfcurf  17955  curf2ndf  17963  yonffthlem  17998  yoniso  18001  dprd2dlem2  19641  dprd2dlem1  19642  dprd2da  19643  mdetunilem9  21767  2ndcctbss  22604  utop2nei  23400  utop3cls  23401  caubl  24470  wlkop  27992  nvop2  28966  nvvop  28967  nvop  29034  phop  29176  fgreu  31005  1stpreimas  31034  gsumhashmul  31312  cvmliftlem1  33243  heiborlem3  35967  rngoi  36053  drngoi  36105  isdrngo1  36110  iscrngo2  36151