![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elimel | Structured version Visualization version GIF version |
Description: Eliminate a membership hypothesis for weak deduction theorem, when special case 𝐵 ∈ 𝐶 is provable. (Contributed by NM, 15-May-1999.) |
Ref | Expression |
---|---|
elimel.1 | ⊢ 𝐵 ∈ 𝐶 |
Ref | Expression |
---|---|
elimel | ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2822 | . 2 ⊢ (𝐴 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶)) | |
2 | eleq1 2822 | . 2 ⊢ (𝐵 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶)) | |
3 | elimel.1 | . 2 ⊢ 𝐵 ∈ 𝐶 | |
4 | 1, 2, 3 | elimhyp 4555 | 1 ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ifcif 4490 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-if 4491 |
This theorem is referenced by: fprg 7105 orduninsuc 7783 oawordeu 8506 oeoa 8548 omopth 8612 unfilem3 9262 inar1 10719 supsr 11056 renegcl 11472 peano5uzti 12601 eluzaddOLD 12806 eluzsubOLD 12807 ltweuz 13875 uzenom 13878 seqfn 13927 seq1 13928 seqp1 13930 sqeqor 14129 binom2 14130 nn0opth2 14181 faclbnd4lem2 14203 hashxp 14343 dvdsle 16200 divalglem7 16289 divalg 16293 gcdaddm 16413 smadiadetr 22047 iblcnlem 25176 ax5seglem8 27934 elimnv 29674 elimnvu 29675 nmlno0i 29785 nmblolbi 29791 blocn 29798 elimphu 29812 ubth 29864 htth 29909 ifhvhv0 30013 normlem6 30106 norm-iii 30131 norm3lemt 30143 ifchhv 30235 hhssablo 30254 hhssnvt 30256 shscl 30309 shslej 30371 shincl 30372 omlsii 30394 pjoml 30427 pjoc2 30430 chm0 30482 chne0 30485 chocin 30486 chj0 30488 chlejb1 30503 chnle 30505 ledi 30531 h1datom 30573 cmbr3 30599 pjoml2 30602 cmcm 30605 cmcm3 30606 lecm 30608 pjmuli 30680 pjige0 30682 pjhfo 30697 pj11 30705 eigre 30826 eigorth 30829 hoddi 30981 nmlnop0 30989 lnopeq 31000 lnopunilem2 31002 nmbdoplb 31016 nmcopex 31020 nmcoplb 31021 lnopcon 31026 lnfn0 31038 lnfnmul 31039 nmcfnex 31044 nmcfnlb 31045 lnfncon 31047 riesz4 31055 riesz1 31056 cnlnadjeu 31069 pjhmop 31141 pjidmco 31172 mdslmd1lem3 31318 mdslmd1lem4 31319 csmdsymi 31325 hatomic 31351 atord 31379 atcvat2 31380 bnj941 33448 bnj944 33614 kur14 33874 abs2sqle 34332 abs2sqlt 34333 onsucconn 34963 onsucsuccmp 34969 sdclem1 36252 mnurnd 42655 bnd2d 47216 |
Copyright terms: Public domain | W3C validator |