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 486	. . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐵)
3	1, 2	eqeltrrd 2842	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵)
4		df-br 5076	. 2 ⊢ ((1st ‘𝐴)𝐵(2nd ‘𝐴) ↔ ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵)
5	3, 4	sylibr 236	1 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → (1st ‘𝐴)𝐵(2nd ‘𝐴))

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121  ⟨cop 4564   class class class wbr 5075  Rel wrel 5626  ‘cfv 6489  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 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pr 5365  ax-un 7682

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-iota 6445  df-fun 6491  df-fv 6497  df-1st 7935  df-2nd 7936

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  24237  utop3cls  24238  func1st2nd  49580  oppfval2  49641  idfullsubc  49665  fulloppf  49667  fthoppf  49668  up1st2nd2  49692  uptra  49719  uptrar  49720  uptr2a  49726  diag1  49808  fuco11bALT  49842  precofvalALT  49872  thincciso  49957  thincciso2  49959  eufunclem  50025