Theorem 1st2ndbr 8065

Description: Express an element of a relation as a relationship between first and second components. (Contributed by Mario Carneiro, 22-Jun-2016.)

Assertion

Ref	Expression
1st2ndbr	⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → (1st ‘𝐴)𝐵(2nd ‘𝐴))

Proof of Theorem 1st2ndbr

Step	Hyp	Ref	Expression
1		1st2nd 8062	. . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
2		simpr 484	. . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐵)
3	1, 2	eqeltrrd 2839	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵)
4		df-br 5148	. 2 ⊢ ((1st ‘𝐴)𝐵(2nd ‘𝐴) ↔ ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵)
5	3, 4	sylibr 234	1 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → (1st ‘𝐴)𝐵(2nd ‘𝐴))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ⟨cop 4636   class class class wbr 5147  Rel wrel 5693  ‘cfv 6562  1^st c1st 8010  2^nd c2nd 8011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fv 6570  df-1st 8012  df-2nd 8013

This theorem is referenced by:  cofuval  17932  cofu1  17934  cofu2  17936  cofucl  17938  cofuass  17939  cofulid  17940  cofurid  17941  funcres  17946  cofull  17987  cofth  17988  isnat2  18002  fuccocl  18020  fucidcl  18021  fuclid  18022  fucrid  18023  fucass  18024  fucsect  18028  fucinv  18029  invfuc  18030  fuciso  18031  natpropd  18032  fucpropd  18033  homahom  18092  homadm  18093  homacd  18094  homadmcd  18095  catciso  18164  prfval  18254  prfcl  18258  prf1st  18259  prf2nd  18260  1st2ndprf  18261  evlfcllem  18277  evlfcl  18278  curf1cl  18284  curf2cl  18287  curfcl  18288  uncf1  18292  uncf2  18293  curfuncf  18294  uncfcurf  18295  diag1cl  18298  diag2cl  18302  curf2ndf  18303  yon1cl  18319  oyon1cl  18327  yonedalem1  18328  yonedalem21  18329  yonedalem3a  18330  yonedalem4c  18333  yonedalem22  18334  yonedalem3b  18335  yonedalem3  18336  yonedainv  18337  yonffthlem  18338  yoniso  18341  utop2nei  24274  utop3cls  24275  thincciso  48848