![]() |
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 5031 | . . 3 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
2 | brabga.2 | . . . 4 ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} | |
3 | 2 | eleq2i 2881 | . . 3 ⊢ (〈𝐴, 𝐵〉 ∈ 𝑅 ↔ 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑}) |
4 | 1, 3 | bitri 278 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑}) |
5 | opelopabga.1 | . . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) | |
6 | 5 | opelopabga 5385 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓)) |
7 | 4, 6 | syl5bb 286 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1538 ∈ wcel 2111 〈cop 4531 class class class wbr 5030 {copab 5092 |
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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 df-opab 5093 |
This theorem is referenced by: braba 5389 brabg 5391 epelg 5431 brcog 5701 fmptco 6868 ofrfval 7397 isfsupp 8821 wemaplem1 8994 oemapval 9130 wemapwe 9144 fpwwe2lem2 10043 fpwwelem 10056 clim 14843 rlim 14844 vdwmc 16304 isstruct2 16485 brssc 17076 isfunc 17126 isfull 17172 isfth 17176 ipole 17760 eqgval 18321 frgpuplem 18890 dvdsr 19392 islindf 20501 ulmval 24975 hpgbr 26554 isausgr 26957 issubgr 27061 isrgr 27349 isrusgr 27351 istrlson 27496 upgrwlkdvspth 27528 ispthson 27531 isspthson 27532 erclwwlkeq 27803 erclwwlkneq 27852 hlimi 28971 isinftm 30860 brfldext 31125 brfinext 31131 metidv 31245 ismntoplly 31376 brae 31610 braew 31611 brfae 31617 satfbrsuc 32726 prv 32788 bj-epelg 34484 bj-ideqgALT 34573 bj-idreseq 34577 bj-idreseqb 34578 bj-ideqg1ALT 34580 brcoss 35836 brcoels 35840 brdmqss 36041 climf 42264 climf2 42308 nelbr 43830 isomgr 44341 iscllaw 44449 iscomlaw 44450 isasslaw 44452 islininds 44855 lindepsnlininds 44861 |
Copyright terms: Public domain | W3C validator |