Theorem 1st2ndbr 7990

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 7987	. . 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 5631  ‘cfv 6494  1^st c1st 7935  2^nd c2nd 7936

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 5232  ax-nul 5242  ax-pr 5372  ax-un 7684

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 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-iota 6450  df-fun 6496  df-fv 6502  df-1st 7937  df-2nd 7938

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  24229  utop3cls  24230  func1st2nd  49567  oppfval2  49628  idfullsubc  49652  fulloppf  49654  fthoppf  49655  up1st2nd2  49679  uptra  49706  uptrar  49707  uptr2a  49713  diag1  49795  fuco11bALT  49829  precofvalALT  49859  thincciso  49944  thincciso2  49946  eufunclem  50012