Theorem 1st2ndbr 7986

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ⟨cop 4574   class class class wbr 5086  Rel wrel 5627  ‘cfv 6490  1^st c1st 7931  2^nd c2nd 7932

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 5231  ax-nul 5241  ax-pr 5368  ax-un 7680

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 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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 7933  df-2nd 7934

This theorem is referenced by:  cofuval  17838  cofu1  17840  cofu2  17842  cofucl  17844  cofuass  17845  cofulid  17846  cofurid  17847  funcres  17852  cofull  17892  cofth  17893  isnat2  17907  fuccocl  17923  fucidcl  17924  fuclid  17925  fucrid  17926  fucass  17927  fucsect  17931  fucinv  17932  invfuc  17933  fuciso  17934  natpropd  17935  fucpropd  17936  homahom  17995  homadm  17996  homacd  17997  homadmcd  17998  catciso  18067  prfval  18154  prfcl  18158  prf1st  18159  prf2nd  18160  1st2ndprf  18161  evlfcllem  18176  evlfcl  18177  curf1cl  18183  curf2cl  18186  curfcl  18187  uncf1  18191  uncf2  18192  curfuncf  18193  uncfcurf  18194  diag1cl  18197  diag2cl  18201  curf2ndf  18202  yon1cl  18218  oyon1cl  18226  yonedalem1  18227  yonedalem21  18228  yonedalem3a  18229  yonedalem4c  18232  yonedalem22  18233  yonedalem3b  18234  yonedalem3  18235  yonedainv  18236  yonffthlem  18237  yoniso  18240  utop2nei  24224  utop3cls  24225  func1st2nd  49548  oppfval2  49609  idfullsubc  49633  fulloppf  49635  fthoppf  49636  up1st2nd2  49660  uptra  49687  uptrar  49688  uptr2a  49694  diag1  49776  fuco11bALT  49810  precofvalALT  49840  thincciso  49925  thincciso2  49927  eufunclem  49993