![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > brabga | Structured version Visualization version GIF version |
Description: The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013.) |
Ref | Expression |
---|---|
opelopabga.1 | ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) |
brabga.2 | ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} |
Ref | Expression |
---|---|
brabga | ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-br 4797 | . . 3 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
2 | brabga.2 | . . . 4 ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} | |
3 | 2 | eleq2i 2823 | . . 3 ⊢ (〈𝐴, 𝐵〉 ∈ 𝑅 ↔ 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑}) |
4 | 1, 3 | bitri 264 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑}) |
5 | opelopabga.1 | . . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) | |
6 | 5 | opelopabga 5130 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓)) |
7 | 4, 6 | syl5bb 272 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1624 ∈ wcel 2131 〈cop 4319 class class class wbr 4796 {copab 4856 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-sep 4925 ax-nul 4933 ax-pr 5047 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-rab 3051 df-v 3334 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-sn 4314 df-pr 4316 df-op 4320 df-br 4797 df-opab 4857 |
This theorem is referenced by: braba 5134 brabg 5136 epelg 5172 brcog 5436 fmptco 6551 ofrfval 7062 isfsupp 8436 wemaplem1 8608 oemapval 8745 wemapwe 8759 fpwwe2lem2 9638 fpwwelem 9651 clim 14416 rlim 14417 vdwmc 15876 isstruct2 16061 brssc 16667 isfunc 16717 isfull 16763 isfth 16767 ipole 17351 eqgval 17836 frgpuplem 18377 dvdsr 18838 islindf 20345 ulmval 24325 hpgbr 25843 isausgr 26250 issubgr 26354 isrgr 26657 isrusgr 26659 istrlson 26805 upgrwlkdvspth 26837 ispthson 26840 isspthson 26841 erclwwlkeq 27133 erclwwlkneq 27190 hlimi 28346 isinftm 30036 metidv 30236 ismntoplly 30370 brae 30605 braew 30606 brfae 30612 brcoss 34501 brcoels 34505 climf 40349 climf2 40393 nelbr 41792 iscllaw 42327 iscomlaw 42328 isasslaw 42330 islininds 42737 lindepsnlininds 42743 |
Copyright terms: Public domain | W3C validator |