| 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 5087 | . . 3 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
| 2 | brabga.2 | . . . 4 ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} | |
| 3 | 2 | eleq2i 2829 | . . 3 ⊢ (〈𝐴, 𝐵〉 ∈ 𝑅 ↔ 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑}) |
| 4 | 1, 3 | bitri 275 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑}) |
| 5 | opelopabga.1 | . . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) | |
| 6 | 5 | opelopabga 5483 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓)) |
| 7 | 4, 6 | bitrid 283 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 〈cop 4574 class class class wbr 5086 {copab 5148 |
| 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 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-ext 2709 ax-sep 5232 ax-pr 5372 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-clel 2812 df-rab 3391 df-v 3432 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-sn 4569 df-pr 4571 df-op 4575 df-br 5087 df-opab 5149 |
| This theorem is referenced by: braba 5487 brabg 5489 epelg 5527 brcog 5817 fmptco 7078 ofrfvalg 7634 isfsupp 9273 wemaplem1 9456 oemapval 9599 wemapwe 9613 fpwwe2lem2 10550 fpwwelem 10563 clim 15451 rlim 15452 vdwmc 16944 isstruct2 17114 brssc 17776 isfunc 17826 isfull 17874 isfth 17878 ipole 18495 eqgval 19147 frgpuplem 19742 dvdsr 20337 islindf 21806 ulmval 26362 hpgbr 28846 isausgr 29251 issubgr 29358 isrgr 29647 isrusgr 29649 istrlson 29792 upgrwlkdvspth 29826 ispthson 29829 isspthson 29830 erclwwlkeq 30107 erclwwlkneq 30156 hlimi 31278 isinftm 33261 brfldext 33809 brfinext 33816 finextfldext 33828 bralgext 33861 fldext2chn 33892 constrextdg2lem 33912 metidv 34056 ismntoplly 34189 brae 34405 braew 34406 brfae 34412 satfbrsuc 35568 prv 35630 bj-epelg 37395 bj-ideqgALT 37492 bj-idreseq 37496 bj-idreseqb 37497 bj-ideqg1ALT 37499 ecqmap 38788 brsucmap 38805 brcoss 38860 brcoels 38864 brdmqss 39069 aks6d1c1p1 42564 climf 46074 climf2 46116 nelbr 47738 iscllaw 48681 iscomlaw 48682 isasslaw 48684 islininds 48938 lindepsnlininds 48944 |
| Copyright terms: Public domain | W3C validator |