Theorem 1st2ndbr 7892

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 7889	. . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩)
2		simpr 485	. . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐵)
3	1, 2	eqeltrrd 2841	. 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵)
4		df-br 5076	. 2 ⊢ ((1st ‘𝐴)𝐵(2nd ‘𝐴) ↔ ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵)
5	3, 4	sylibr 233	1 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → (1st ‘𝐴)𝐵(2nd ‘𝐴))

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107  ⟨cop 4568   class class class wbr 5075  Rel wrel 5595  ‘cfv 6437  1^st c1st 7838  2^nd c2nd 7839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-iota 6395  df-fun 6439  df-fv 6445  df-1st 7840  df-2nd 7841

This theorem is referenced by:  cofuval  17606  cofu1  17608  cofu2  17610  cofucl  17612  cofuass  17613  cofulid  17614  cofurid  17615  funcres  17620  cofull  17659  cofth  17660  isnat2  17673  fuccocl  17691  fucidcl  17692  fuclid  17693  fucrid  17694  fucass  17695  fucsect  17699  fucinv  17700  invfuc  17701  fuciso  17702  natpropd  17703  fucpropd  17704  homahom  17763  homadm  17764  homacd  17765  homadmcd  17766  catciso  17835  prfval  17925  prfcl  17929  prf1st  17930  prf2nd  17931  1st2ndprf  17932  evlfcllem  17948  evlfcl  17949  curf1cl  17955  curf2cl  17958  curfcl  17959  uncf1  17963  uncf2  17964  curfuncf  17965  uncfcurf  17966  diag1cl  17969  diag2cl  17973  curf2ndf  17974  yon1cl  17990  oyon1cl  17998  yonedalem1  17999  yonedalem21  18000  yonedalem3a  18001  yonedalem4c  18004  yonedalem22  18005  yonedalem3b  18006  yonedalem3  18007  yonedainv  18008  yonffthlem  18009  yoniso  18012  utop2nei  23411  utop3cls  23412  thincciso  46341