Theorem 1st2nd 7585

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1520   ∈ wcel 2079  Vcvv 3432   ⊆ wss 3854  ⟨cop 4472   × cxp 5433  Rel wrel 5440  ‘cfv 6217  1^st c1st 7534  2^nd c2nd 7535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-sbc 3702  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-opab 5019  df-mpt 5036  df-id 5340  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-iota 6181  df-fun 6219  df-fv 6225  df-1st 7536  df-2nd 7537

This theorem is referenced by:  2ndrn  7587  1st2ndbr  7588  funfv1st2nd  7592  funelss  7593  elopabi  7607  cnvf1olem  7652  ordpinq  10200  addassnq  10215  mulassnq  10216  distrnq  10218  mulidnq  10220  recmulnq  10221  ltexnq  10232  fsumcnv  14949  fprodcnv  15158  cofulid  16977  cofurid  16978  idffth  17020  cofull  17021  cofth  17022  ressffth  17025  isnat2  17035  nat1st2nd  17038  homadmcd  17119  catciso  17184  prf1st  17271  prf2nd  17272  1st2ndprf  17273  curfuncf  17305  uncfcurf  17306  curf2ndf  17314  yonffthlem  17349  yoniso  17352  dprd2dlem2  18867  dprd2dlem1  18868  dprd2da  18869  mdetunilem9  20901  2ndcctbss  21735  utop2nei  22530  utop3cls  22531  caubl  23582  wlkop  27080  nvop2  28064  nvvop  28065  nvop  28132  phop  28274  fgreu  30080  1stpreimas  30102  cvmliftlem1  32096  heiborlem3  34569  rngoi  34655  drngoi  34707  isdrngo1  34712  iscrngo2  34753