Theorem 1st2ndbr 8021

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 8018	. . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
2		simpr 484	. . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐵)
3	1, 2	eqeltrrd 2829	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵)
4		df-br 5108	. 2 ⊢ ((1st ‘𝐴)𝐵(2nd ‘𝐴) ↔ ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵)
5	3, 4	sylibr 234	1 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → (1st ‘𝐴)𝐵(2nd ‘𝐴))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ⟨cop 4595   class class class wbr 5107  Rel wrel 5643  ‘cfv 6511  1^st c1st 7966  2^nd c2nd 7967

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6464  df-fun 6513  df-fv 6519  df-1st 7968  df-2nd 7969

This theorem is referenced by:  cofuval  17844  cofu1  17846  cofu2  17848  cofucl  17850  cofuass  17851  cofulid  17852  cofurid  17853  funcres  17858  cofull  17898  cofth  17899  isnat2  17913  fuccocl  17929  fucidcl  17930  fuclid  17931  fucrid  17932  fucass  17933  fucsect  17937  fucinv  17938  invfuc  17939  fuciso  17940  natpropd  17941  fucpropd  17942  homahom  18001  homadm  18002  homacd  18003  homadmcd  18004  catciso  18073  prfval  18160  prfcl  18164  prf1st  18165  prf2nd  18166  1st2ndprf  18167  evlfcllem  18182  evlfcl  18183  curf1cl  18189  curf2cl  18192  curfcl  18193  uncf1  18197  uncf2  18198  curfuncf  18199  uncfcurf  18200  diag1cl  18203  diag2cl  18207  curf2ndf  18208  yon1cl  18224  oyon1cl  18232  yonedalem1  18233  yonedalem21  18234  yonedalem3a  18235  yonedalem4c  18238  yonedalem22  18239  yonedalem3b  18240  yonedalem3  18241  yonedainv  18242  yonffthlem  18243  yoniso  18246  utop2nei  24138  utop3cls  24139  func1st2nd  49065  oppfval2  49126  idfullsubc  49150  fulloppf  49152  fthoppf  49153  up1st2nd2  49177  uptra  49204  uptrar  49205  uptr2a  49211  diag1  49293  fuco11bALT  49327  precofvalALT  49357  thincciso  49442  thincciso2  49444  eufunclem  49510