Theorem 1st2ndbr 7984

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ⟨cop 4584   class class class wbr 5096  Rel wrel 5627  ‘cfv 6490  1^st c1st 7929  2^nd c2nd 7930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fv 6498  df-1st 7931  df-2nd 7932

This theorem is referenced by:  cofuval  17804  cofu1  17806  cofu2  17808  cofucl  17810  cofuass  17811  cofulid  17812  cofurid  17813  funcres  17818  cofull  17858  cofth  17859  isnat2  17873  fuccocl  17889  fucidcl  17890  fuclid  17891  fucrid  17892  fucass  17893  fucsect  17897  fucinv  17898  invfuc  17899  fuciso  17900  natpropd  17901  fucpropd  17902  homahom  17961  homadm  17962  homacd  17963  homadmcd  17964  catciso  18033  prfval  18120  prfcl  18124  prf1st  18125  prf2nd  18126  1st2ndprf  18127  evlfcllem  18142  evlfcl  18143  curf1cl  18149  curf2cl  18152  curfcl  18153  uncf1  18157  uncf2  18158  curfuncf  18159  uncfcurf  18160  diag1cl  18163  diag2cl  18167  curf2ndf  18168  yon1cl  18184  oyon1cl  18192  yonedalem1  18193  yonedalem21  18194  yonedalem3a  18195  yonedalem4c  18198  yonedalem22  18199  yonedalem3b  18200  yonedalem3  18201  yonedainv  18202  yonffthlem  18203  yoniso  18206  utop2nei  24192  utop3cls  24193  func1st2nd  49263  oppfval2  49324  idfullsubc  49348  fulloppf  49350  fthoppf  49351  up1st2nd2  49375  uptra  49402  uptrar  49403  uptr2a  49409  diag1  49491  fuco11bALT  49525  precofvalALT  49555  thincciso  49640  thincciso2  49642  eufunclem  49708