Theorem 1st2ndbr 7988

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ⟨cop 4587   class class class wbr 5099  Rel wrel 5630  ‘cfv 6493  1^st c1st 7933  2^nd c2nd 7934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6449  df-fun 6495  df-fv 6501  df-1st 7935  df-2nd 7936

This theorem is referenced by:  cofuval  17810  cofu1  17812  cofu2  17814  cofucl  17816  cofuass  17817  cofulid  17818  cofurid  17819  funcres  17824  cofull  17864  cofth  17865  isnat2  17879  fuccocl  17895  fucidcl  17896  fuclid  17897  fucrid  17898  fucass  17899  fucsect  17903  fucinv  17904  invfuc  17905  fuciso  17906  natpropd  17907  fucpropd  17908  homahom  17967  homadm  17968  homacd  17969  homadmcd  17970  catciso  18039  prfval  18126  prfcl  18130  prf1st  18131  prf2nd  18132  1st2ndprf  18133  evlfcllem  18148  evlfcl  18149  curf1cl  18155  curf2cl  18158  curfcl  18159  uncf1  18163  uncf2  18164  curfuncf  18165  uncfcurf  18166  diag1cl  18169  diag2cl  18173  curf2ndf  18174  yon1cl  18190  oyon1cl  18198  yonedalem1  18199  yonedalem21  18200  yonedalem3a  18201  yonedalem4c  18204  yonedalem22  18205  yonedalem3b  18206  yonedalem3  18207  yonedainv  18208  yonffthlem  18209  yoniso  18212  utop2nei  24198  utop3cls  24199  func1st2nd  49388  oppfval2  49449  idfullsubc  49473  fulloppf  49475  fthoppf  49476  up1st2nd2  49500  uptra  49527  uptrar  49528  uptr2a  49534  diag1  49616  fuco11bALT  49650  precofvalALT  49680  thincciso  49765  thincciso2  49767  eufunclem  49833