![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 1st2ndbr | Structured version Visualization version GIF version |
Description: Express an element of a relation as a relationship between first and second components. (Contributed by Mario Carneiro, 22-Jun-2016.) |
Ref | Expression |
---|---|
1st2ndbr | ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → (1st ‘𝐴)𝐵(2nd ‘𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1st2nd 8022 | . . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩) | |
2 | simpr 486 | . . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐵) | |
3 | 1, 2 | eqeltrrd 2835 | . 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵) |
4 | df-br 5149 | . 2 ⊢ ((1st ‘𝐴)𝐵(2nd ‘𝐴) ↔ ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵) | |
5 | 3, 4 | sylibr 233 | 1 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → (1st ‘𝐴)𝐵(2nd ‘𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 ∈ wcel 2107 ⟨cop 4634 class class class wbr 5148 Rel wrel 5681 ‘cfv 6541 1st c1st 7970 2nd c2nd 7971 |
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 2704 ax-sep 5299 ax-nul 5306 ax-pr 5427 ax-un 7722 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-iota 6493 df-fun 6543 df-fv 6549 df-1st 7972 df-2nd 7973 |
This theorem is referenced by: cofuval 17829 cofu1 17831 cofu2 17833 cofucl 17835 cofuass 17836 cofulid 17837 cofurid 17838 funcres 17843 cofull 17882 cofth 17883 isnat2 17896 fuccocl 17914 fucidcl 17915 fuclid 17916 fucrid 17917 fucass 17918 fucsect 17922 fucinv 17923 invfuc 17924 fuciso 17925 natpropd 17926 fucpropd 17927 homahom 17986 homadm 17987 homacd 17988 homadmcd 17989 catciso 18058 prfval 18148 prfcl 18152 prf1st 18153 prf2nd 18154 1st2ndprf 18155 evlfcllem 18171 evlfcl 18172 curf1cl 18178 curf2cl 18181 curfcl 18182 uncf1 18186 uncf2 18187 curfuncf 18188 uncfcurf 18189 diag1cl 18192 diag2cl 18196 curf2ndf 18197 yon1cl 18213 oyon1cl 18221 yonedalem1 18222 yonedalem21 18223 yonedalem3a 18224 yonedalem4c 18227 yonedalem22 18228 yonedalem3b 18229 yonedalem3 18230 yonedainv 18231 yonffthlem 18232 yoniso 18235 utop2nei 23747 utop3cls 23748 thincciso 47623 |
Copyright terms: Public domain | W3C validator |