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 5032 | . . 3 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ 𝑅) | |
2 | brabga.2 | . . . 4 ⊢ 𝑅 = {〈𝑥, 𝑦〉 ∣ 𝜑} | |
3 | 2 | eleq2i 2825 | . . 3 ⊢ (〈𝐴, 𝐵〉 ∈ 𝑅 ↔ 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑}) |
4 | 1, 3 | bitri 278 | . 2 ⊢ (𝐴𝑅𝐵 ↔ 〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑}) |
5 | opelopabga.1 | . . 3 ⊢ ((𝑥 = 𝐴 ∧ 𝑦 = 𝐵) → (𝜑 ↔ 𝜓)) | |
6 | 5 | opelopabga 5389 | . 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (〈𝐴, 𝐵〉 ∈ {〈𝑥, 𝑦〉 ∣ 𝜑} ↔ 𝜓)) |
7 | 4, 6 | syl5bb 286 | 1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴𝑅𝐵 ↔ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1542 ∈ wcel 2114 〈cop 4523 class class class wbr 5031 {copab 5093 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2711 ax-sep 5168 ax-nul 5175 ax-pr 5297 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-sb 2075 df-clab 2718 df-cleq 2731 df-clel 2812 df-v 3401 df-dif 3847 df-un 3849 df-nul 4213 df-if 4416 df-sn 4518 df-pr 4520 df-op 4524 df-br 5032 df-opab 5094 |
This theorem is referenced by: braba 5393 brabg 5395 epelg 5436 brcog 5710 fmptco 6904 ofrfvalg 7435 isfsupp 8913 wemaplem1 9086 oemapval 9222 wemapwe 9236 fpwwe2lem2 10135 fpwwelem 10148 clim 14944 rlim 14945 vdwmc 16417 isstruct2 16599 brssc 17192 isfunc 17242 isfull 17288 isfth 17292 ipole 17887 eqgval 18450 frgpuplem 19019 dvdsr 19521 islindf 20631 ulmval 25130 hpgbr 26709 isausgr 27112 issubgr 27216 isrgr 27504 isrusgr 27506 istrlson 27651 upgrwlkdvspth 27683 ispthson 27686 isspthson 27687 erclwwlkeq 27958 erclwwlkneq 28007 hlimi 29126 isinftm 31015 brfldext 31297 brfinext 31303 metidv 31417 ismntoplly 31548 brae 31782 braew 31783 brfae 31789 satfbrsuc 32902 prv 32964 bj-epelg 34884 bj-ideqgALT 34973 bj-idreseq 34977 bj-idreseqb 34978 bj-ideqg1ALT 34980 brcoss 36200 brcoels 36204 brdmqss 36405 climf 42728 climf2 42772 nelbr 44329 isomgr 44839 iscllaw 44947 iscomlaw 44948 isasslaw 44950 islininds 45351 lindepsnlininds 45357 |
Copyright terms: Public domain | W3C validator |