| 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 5479 | . 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 5231 ax-pr 5368 |
| 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 5483 brabg 5485 epelg 5523 brcog 5813 fmptco 7074 ofrfvalg 7630 isfsupp 9269 wemaplem1 9452 oemapval 9593 wemapwe 9607 fpwwe2lem2 10544 fpwwelem 10557 clim 15445 rlim 15446 vdwmc 16938 isstruct2 17108 brssc 17770 isfunc 17820 isfull 17868 isfth 17872 ipole 18489 eqgval 19141 frgpuplem 19736 dvdsr 20331 islindf 21800 ulmval 26356 hpgbr 28840 isausgr 29245 issubgr 29352 isrgr 29641 isrusgr 29643 istrlson 29786 upgrwlkdvspth 29820 ispthson 29823 isspthson 29824 erclwwlkeq 30101 erclwwlkneq 30150 hlimi 31272 isinftm 33255 brfldext 33803 brfinext 33810 finextfldext 33822 bralgext 33855 fldext2chn 33886 constrextdg2lem 33906 metidv 34050 ismntoplly 34183 brae 34399 braew 34400 brfae 34406 satfbrsuc 35562 prv 35624 bj-epelg 37381 bj-ideqgALT 37478 bj-idreseq 37482 bj-idreseqb 37483 bj-ideqg1ALT 37485 ecqmap 38774 brsucmap 38791 brcoss 38846 brcoels 38850 brdmqss 39055 aks6d1c1p1 42550 climf 46060 climf2 46102 nelbr 47724 iscllaw 48667 iscomlaw 48668 isasslaw 48670 islininds 48924 lindepsnlininds 48930 |
| Copyright terms: Public domain | W3C validator |