Theorem 1st2nd 7983

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3440   ⊆ wss 3901  ⟨cop 4586   × cxp 5622  Rel wrel 5629  ‘cfv 6492  1^st c1st 7931  2^nd c2nd 7932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-1st 7933  df-2nd 7934

This theorem is referenced by:  2ndrn  7985  1st2ndbr  7986  funfv1st2nd  7990  funelss  7991  elopabi  8006  cnvf1olem  8052  ordpinq  10854  addassnq  10869  mulassnq  10870  distrnq  10872  mulidnq  10874  recmulnq  10875  ltexnq  10886  fsumcnv  15696  fprodcnv  15906  cofulid  17814  cofurid  17815  idffth  17859  cofull  17860  cofth  17861  ressffth  17864  isnat2  17875  nat1st2nd  17878  homadmcd  17966  catciso  18035  prf1st  18127  prf2nd  18128  1st2ndprf  18129  curfuncf  18161  uncfcurf  18162  curf2ndf  18170  yonffthlem  18205  yoniso  18208  dprd2dlem2  19971  dprd2dlem1  19972  dprd2da  19973  mdetunilem9  22564  2ndcctbss  23399  utop2nei  24194  utop3cls  24195  caubl  25264  wlkop  29701  nvop2  30683  nvvop  30684  nvop  30751  phop  30893  fgreu  32750  1stpreimas  32785  gsumhashmul  33150  cvmliftlem1  35479  heiborlem3  38010  rngoi  38096  drngoi  38148  isdrngo1  38153  iscrngo2  38194  tposideq  49129  cic1st2nd  49288  cofu1st2nd  49333  oppfval2  49378  oppfoppc2  49383  idfth  49399  up1st2nd  49426  up1st2ndr  49427  uptrlem2  49452  uptra  49456  uobeqw  49460  uobeq  49461  uptr2a  49463  diag1  49545  fuco11bALT  49579  fuco22nat  49587  fucocolem4  49597  precofvalALT  49609  prcoftposcurfucoa  49625  prcofdiag1  49634  prcofdiag  49635  oppfdiag1  49655  oppfdiag  49657  termcfuncval  49773  diagffth  49779  lmddu  49908