Theorem 1st2nd 8077

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 5663	. . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
2		ssel2 3908	. . 3 ⊢ ((𝐵 ⊆ (V × V) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
3	1, 2	sylanb 593	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
4		1st2nd2 8067	. 2 ⊢ (𝐴 ∈ (V × V) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
5	3, 4	syl 18	1 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900  ⟨cop 4838   × cxp 5654  Rel wrel 5661  ‘cfv 6561  1^st c1st 8026  2^nd c2nd 8027

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396  ax-un 7778

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-iota 6515  df-fun 6563  df-fv 6569  df-1st 8028  df-2nd 8029

This theorem is used by:  2ndrn  8079  1st2ndbr  8080  funfv1st2nd  8085  funelss  8086  elopabi  8101  cnvf1olem  8151  ordpinq  11058  addassnq  11073  mulassnq  11074  distrnq  11076  mulidnq  11078  recmulnq  11079  ltexnq  11090  fsumcnv  15971  fprodcnv  16182  cofulid  18097  cofurid  18098  idffth  18142  cofull  18143  cofth  18144  ressffth  18147  isnat2  18158  nat1st2nd  18161  homadmcd  18249  catciso  18318  prf1st  18410  prf2nd  18411  1st2ndprf  18412  curfuncf  18444  uncfcurf  18445  curf2ndf  18453  yonffthlem  18488  yoniso  18491  dprd2dlem2  20289  dprd2dlem1  20290  dprd2da  20291  mdetunilem9  22968  2ndcctbss  23807  utop2nei  24602  utop3cls  24603  caubl  25662  wlkop  30241  nvop2  31243  nvvop  31244  nvop  31311  phop  31453  fgreu  33340  1stpreimas  33373  gsumhashmul  33704  cvmliftlem1  36230  heiborlem3  38950  rngoi  39036  drngoi  39088  isdrngo1  39093  iscrngo2  39134  tposideq  50216  cic1st2nd  50376  cofu1st2nd  50422  oppfval2  50468  oppfoppc2  50473  idfth  50489  up1st2nd  50516  up1st2ndr  50517  uptrlem2  50542  uptra  50546  uobeqw  50550  uobeq  50551  uptr2a  50553  diag1  50641  fuco11bALT  50675  fuco22nat  50683  fucocolem4  50693  precofvalALT  50718  prcoftposcurfucoa  50734  prcofdiag1  50743  prcofdiag  50744  oppfdiag1  50764  oppfdiag  50766  termcfuncval  50882  diagffth  50891  lmddu  51065