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 2820 | . 2 ⊢ (𝐴 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶)) | |
2 | eleq1 2820 | . 2 ⊢ (𝐵 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶)) | |
3 | elimel.1 | . 2 ⊢ 𝐵 ∈ 𝐶 | |
4 | 1, 2, 3 | elimhyp 4479 | 1 ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 ifcif 4414 |
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 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-if 4415 |
This theorem is referenced by: fprg 6927 orduninsuc 7577 oawordeu 8212 oeoa 8254 omopth 8316 unfilem3 8858 inar1 10275 supsr 10612 renegcl 11027 peano5uzti 12153 eluzadd 12355 eluzsub 12356 ltweuz 13420 uzenom 13423 seqfn 13472 seq1 13473 seqp1 13475 sqeqor 13670 binom2 13671 nn0opth2 13724 faclbnd4lem2 13746 hashxp 13887 dvdsle 15755 divalglem7 15844 divalg 15848 gcdaddm 15968 smadiadetr 21426 iblcnlem 24541 ax5seglem8 26882 elimnv 28618 elimnvu 28619 nmlno0i 28729 nmblolbi 28735 blocn 28742 elimphu 28756 ubth 28808 htth 28853 ifhvhv0 28957 normlem6 29050 norm-iii 29075 norm3lemt 29087 ifchhv 29179 hhssablo 29198 hhssnvt 29200 shscl 29253 shslej 29315 shincl 29316 omlsii 29338 pjoml 29371 pjoc2 29374 chm0 29426 chne0 29429 chocin 29430 chj0 29432 chlejb1 29447 chnle 29449 ledi 29475 h1datom 29517 cmbr3 29543 pjoml2 29546 cmcm 29549 cmcm3 29550 lecm 29552 pjmuli 29624 pjige0 29626 pjhfo 29641 pj11 29649 eigre 29770 eigorth 29773 hoddi 29925 nmlnop0 29933 lnopeq 29944 lnopunilem2 29946 nmbdoplb 29960 nmcopex 29964 nmcoplb 29965 lnopcon 29970 lnfn0 29982 lnfnmul 29983 nmcfnex 29988 nmcfnlb 29989 lnfncon 29991 riesz4 29999 riesz1 30000 cnlnadjeu 30013 pjhmop 30085 pjidmco 30116 mdslmd1lem3 30262 mdslmd1lem4 30263 csmdsymi 30269 hatomic 30295 atord 30323 atcvat2 30324 bnj941 32323 bnj944 32489 kur14 32749 abs2sqle 33209 abs2sqlt 33210 onsucconn 34265 onsucsuccmp 34271 sdclem1 35524 mnurnd 41443 bnd2d 45840 |
Copyright terms: Public domain | W3C validator |