Theorem 1st2nd 8018

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 5645	. . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
2		ssel2 3941	. . 3 ⊢ ((𝐵 ⊆ (V × V) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
3	1, 2	sylanb 581	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
4		1st2nd2 8007	. 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 3447   ⊆ wss 3914  ⟨cop 4595   × cxp 5636  Rel wrel 5643  ‘cfv 6511  1^st c1st 7966  2^nd c2nd 7967

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 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fv 6519  df-1st 7968  df-2nd 7969

This theorem is referenced by:  2ndrn  8020  1st2ndbr  8021  funfv1st2nd  8025  funelss  8026  elopabi  8041  cnvf1olem  8089  ordpinq  10896  addassnq  10911  mulassnq  10912  distrnq  10914  mulidnq  10916  recmulnq  10917  ltexnq  10928  fsumcnv  15739  fprodcnv  15949  cofulid  17852  cofurid  17853  idffth  17897  cofull  17898  cofth  17899  ressffth  17902  isnat2  17913  nat1st2nd  17916  homadmcd  18004  catciso  18073  prf1st  18165  prf2nd  18166  1st2ndprf  18167  curfuncf  18199  uncfcurf  18200  curf2ndf  18208  yonffthlem  18243  yoniso  18246  dprd2dlem2  19972  dprd2dlem1  19973  dprd2da  19974  mdetunilem9  22507  2ndcctbss  23342  utop2nei  24138  utop3cls  24139  caubl  25208  wlkop  29556  nvop2  30537  nvvop  30538  nvop  30605  phop  30747  fgreu  32596  1stpreimas  32629  gsumhashmul  33001  cvmliftlem1  35272  heiborlem3  37807  rngoi  37893  drngoi  37945  isdrngo1  37950  iscrngo2  37991  tposideq  48876  cic1st2nd  49036  cofu1st2nd  49081  oppfval2  49126  oppfoppc2  49131  idfth  49147  up1st2nd  49174  up1st2ndr  49175  uptrlem2  49200  uptra  49204  uobeqw  49208  uobeq  49209  uptr2a  49211  diag1  49293  fuco11bALT  49327  fuco22nat  49335  fucocolem4  49345  precofvalALT  49357  prcoftposcurfucoa  49373  prcofdiag1  49382  prcofdiag  49383  oppfdiag1  49403  oppfdiag  49405  termcfuncval  49521  diagffth  49527  lmddu  49656