Theorem 1st2ndbr 8024

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ⟨cop 4598   class class class wbr 5110  Rel wrel 5646  ‘cfv 6514  1^st c1st 7969  2^nd c2nd 7970

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 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-iota 6467  df-fun 6516  df-fv 6522  df-1st 7971  df-2nd 7972

This theorem is referenced by:  cofuval  17851  cofu1  17853  cofu2  17855  cofucl  17857  cofuass  17858  cofulid  17859  cofurid  17860  funcres  17865  cofull  17905  cofth  17906  isnat2  17920  fuccocl  17936  fucidcl  17937  fuclid  17938  fucrid  17939  fucass  17940  fucsect  17944  fucinv  17945  invfuc  17946  fuciso  17947  natpropd  17948  fucpropd  17949  homahom  18008  homadm  18009  homacd  18010  homadmcd  18011  catciso  18080  prfval  18167  prfcl  18171  prf1st  18172  prf2nd  18173  1st2ndprf  18174  evlfcllem  18189  evlfcl  18190  curf1cl  18196  curf2cl  18199  curfcl  18200  uncf1  18204  uncf2  18205  curfuncf  18206  uncfcurf  18207  diag1cl  18210  diag2cl  18214  curf2ndf  18215  yon1cl  18231  oyon1cl  18239  yonedalem1  18240  yonedalem21  18241  yonedalem3a  18242  yonedalem4c  18245  yonedalem22  18246  yonedalem3b  18247  yonedalem3  18248  yonedainv  18249  yonffthlem  18250  yoniso  18253  utop2nei  24145  utop3cls  24146  func1st2nd  49069  oppfval2  49130  idfullsubc  49154  fulloppf  49156  fthoppf  49157  up1st2nd2  49181  uptra  49208  uptrar  49209  uptr2a  49215  diag1  49297  fuco11bALT  49331  precofvalALT  49361  thincciso  49446  thincciso2  49448  eufunclem  49514