![]() |
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 8027 | . . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 = ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩) | |
2 | simpr 483 | . . 3 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐵) | |
3 | 1, 2 | eqeltrrd 2832 | . 2 ⊢ ((Rel 𝐵 ∧ 𝐴 ∈ 𝐵) → ⟨(1st ‘𝐴), (2nd ‘𝐴)⟩ ∈ 𝐵) |
4 | df-br 5148 | . 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 394 ∈ wcel 2104 ⟨cop 4633 class class class wbr 5147 Rel wrel 5680 ‘cfv 6542 1st c1st 7975 2nd c2nd 7976 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pr 5426 ax-un 7727 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ral 3060 df-rex 3069 df-rab 3431 df-v 3474 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-iota 6494 df-fun 6544 df-fv 6550 df-1st 7977 df-2nd 7978 |
This theorem is referenced by: cofuval 17836 cofu1 17838 cofu2 17840 cofucl 17842 cofuass 17843 cofulid 17844 cofurid 17845 funcres 17850 cofull 17889 cofth 17890 isnat2 17903 fuccocl 17921 fucidcl 17922 fuclid 17923 fucrid 17924 fucass 17925 fucsect 17929 fucinv 17930 invfuc 17931 fuciso 17932 natpropd 17933 fucpropd 17934 homahom 17993 homadm 17994 homacd 17995 homadmcd 17996 catciso 18065 prfval 18155 prfcl 18159 prf1st 18160 prf2nd 18161 1st2ndprf 18162 evlfcllem 18178 evlfcl 18179 curf1cl 18185 curf2cl 18188 curfcl 18189 uncf1 18193 uncf2 18194 curfuncf 18195 uncfcurf 18196 diag1cl 18199 diag2cl 18203 curf2ndf 18204 yon1cl 18220 oyon1cl 18228 yonedalem1 18229 yonedalem21 18230 yonedalem3a 18231 yonedalem4c 18234 yonedalem22 18235 yonedalem3b 18236 yonedalem3 18237 yonedainv 18238 yonffthlem 18239 yoniso 18242 utop2nei 23975 utop3cls 23976 thincciso 47756 |
Copyright terms: Public domain | W3C validator |