Theorem 1st2nd 7788

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2112  Vcvv 3398   ⊆ wss 3853  ⟨cop 4533   × cxp 5534  Rel wrel 5541  ‘cfv 6358  1^st c1st 7737  2^nd c2nd 7738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-iota 6316  df-fun 6360  df-fv 6366  df-1st 7739  df-2nd 7740

This theorem is referenced by:  2ndrn  7790  1st2ndbr  7791  funfv1st2nd  7795  funelss  7796  elopabi  7810  cnvf1olem  7856  ordpinq  10522  addassnq  10537  mulassnq  10538  distrnq  10540  mulidnq  10542  recmulnq  10543  ltexnq  10554  fsumcnv  15300  fprodcnv  15508  cofulid  17350  cofurid  17351  idffth  17394  cofull  17395  cofth  17396  ressffth  17399  isnat2  17409  nat1st2nd  17412  homadmcd  17502  catciso  17571  prf1st  17665  prf2nd  17666  1st2ndprf  17667  curfuncf  17700  uncfcurf  17701  curf2ndf  17709  yonffthlem  17744  yoniso  17747  dprd2dlem2  19381  dprd2dlem1  19382  dprd2da  19383  mdetunilem9  21471  2ndcctbss  22306  utop2nei  23102  utop3cls  23103  caubl  24159  wlkop  27669  nvop2  28643  nvvop  28644  nvop  28711  phop  28853  fgreu  30683  1stpreimas  30712  gsumhashmul  30989  cvmliftlem1  32914  heiborlem3  35657  rngoi  35743  drngoi  35795  isdrngo1  35800  iscrngo2  35841