Theorem 1st2nd 8051

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 5657	. . 3 ⊢ (Rel 𝐵 ↔ 𝐵 ⊆ (V × V))
2		ssel2 3903	. . 3 ⊢ ((𝐵 ⊆ (V × V) ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
3	1, 2	sylanb 593	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (V × V))
4		1st2nd2 8041	. 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 1569   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3895  ⟨cop 4834   × cxp 5648  Rel wrel 5655  ‘cfv 6539  1^st c1st 8000  2^nd c2nd 8001

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-iota 6494  df-fun 6541  df-fv 6547  df-1st 8002  df-2nd 8003

This theorem is used by:  2ndrn  8053  1st2ndbr  8054  funfv1st2nd  8058  funelss  8059  elopabi  8074  cnvf1olem  8124  ordpinq  11032  addassnq  11047  mulassnq  11048  distrnq  11050  mulidnq  11052  recmulnq  11053  ltexnq  11064  fsumcnv  15945  fprodcnv  16156  cofulid  18071  cofurid  18072  idffth  18116  cofull  18117  cofth  18118  ressffth  18121  isnat2  18132  nat1st2nd  18135  homadmcd  18223  catciso  18292  prf1st  18384  prf2nd  18385  1st2ndprf  18386  curfuncf  18418  uncfcurf  18419  curf2ndf  18427  yonffthlem  18462  yoniso  18465  dprd2dlem2  20262  dprd2dlem1  20263  dprd2da  20264  mdetunilem9  22941  2ndcctbss  23780  utop2nei  24575  utop3cls  24576  caubl  25635  wlkop  30214  nvop2  31216  nvvop  31217  nvop  31284  phop  31426  fgreu  33313  1stpreimas  33347  gsumhashmul  33675  cvmliftlem1  36137  heiborlem3  38841  rngoi  38927  drngoi  38979  isdrngo1  38984  iscrngo2  39025  tposideq  50095  cic1st2nd  50255  cofu1st2nd  50301  oppfval2  50347  oppfoppc2  50352  idfth  50368  up1st2nd  50395  up1st2ndr  50396  uptrlem2  50421  uptra  50425  uobeqw  50429  uobeq  50430  uptr2a  50432  diag1  50520  fuco11bALT  50554  fuco22nat  50562  fucocolem4  50572  precofvalALT  50597  prcoftposcurfucoa  50613  prcofdiag1  50622  prcofdiag  50623  oppfdiag1  50643  oppfdiag  50645  termcfuncval  50761  diagffth  50770  lmddu  50944