Theorem 1st2ndbr 7998

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ⟨cop 4588   class class class wbr 5100  Rel wrel 5639  ‘cfv 6502  1^st c1st 7943  2^nd c2nd 7944

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 5245  ax-nul 5255  ax-pr 5381  ax-un 7692

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6458  df-fun 6504  df-fv 6510  df-1st 7945  df-2nd 7946

This theorem is referenced by:  cofuval  17820  cofu1  17822  cofu2  17824  cofucl  17826  cofuass  17827  cofulid  17828  cofurid  17829  funcres  17834  cofull  17874  cofth  17875  isnat2  17889  fuccocl  17905  fucidcl  17906  fuclid  17907  fucrid  17908  fucass  17909  fucsect  17913  fucinv  17914  invfuc  17915  fuciso  17916  natpropd  17917  fucpropd  17918  homahom  17977  homadm  17978  homacd  17979  homadmcd  17980  catciso  18049  prfval  18136  prfcl  18140  prf1st  18141  prf2nd  18142  1st2ndprf  18143  evlfcllem  18158  evlfcl  18159  curf1cl  18165  curf2cl  18168  curfcl  18169  uncf1  18173  uncf2  18174  curfuncf  18175  uncfcurf  18176  diag1cl  18179  diag2cl  18183  curf2ndf  18184  yon1cl  18200  oyon1cl  18208  yonedalem1  18209  yonedalem21  18210  yonedalem3a  18211  yonedalem4c  18214  yonedalem22  18215  yonedalem3b  18216  yonedalem3  18217  yonedainv  18218  yonffthlem  18219  yoniso  18222  utop2nei  24211  utop3cls  24212  func1st2nd  49464  oppfval2  49525  idfullsubc  49549  fulloppf  49551  fthoppf  49552  up1st2nd2  49576  uptra  49603  uptrar  49604  uptr2a  49610  diag1  49692  fuco11bALT  49726  precofvalALT  49756  thincciso  49841  thincciso2  49843  eufunclem  49909