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 2827 | . 2 ⊢ (𝐴 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶)) | |
2 | eleq1 2827 | . 2 ⊢ (𝐵 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶)) | |
3 | elimel.1 | . 2 ⊢ 𝐵 ∈ 𝐶 | |
4 | 1, 2, 3 | elimhyp 4525 | 1 ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 ifcif 4460 |
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 2710 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-clel 2817 df-if 4461 |
This theorem is referenced by: fprg 7036 orduninsuc 7699 oawordeu 8395 oeoa 8437 omopth 8501 unfilem3 9089 inar1 10540 supsr 10877 renegcl 11293 peano5uzti 12419 eluzadd 12622 eluzsub 12623 ltweuz 13690 uzenom 13693 seqfn 13742 seq1 13743 seqp1 13745 sqeqor 13941 binom2 13942 nn0opth2 13995 faclbnd4lem2 14017 hashxp 14158 dvdsle 16028 divalglem7 16117 divalg 16121 gcdaddm 16241 smadiadetr 21833 iblcnlem 24962 ax5seglem8 27313 elimnv 29054 elimnvu 29055 nmlno0i 29165 nmblolbi 29171 blocn 29178 elimphu 29192 ubth 29244 htth 29289 ifhvhv0 29393 normlem6 29486 norm-iii 29511 norm3lemt 29523 ifchhv 29615 hhssablo 29634 hhssnvt 29636 shscl 29689 shslej 29751 shincl 29752 omlsii 29774 pjoml 29807 pjoc2 29810 chm0 29862 chne0 29865 chocin 29866 chj0 29868 chlejb1 29883 chnle 29885 ledi 29911 h1datom 29953 cmbr3 29979 pjoml2 29982 cmcm 29985 cmcm3 29986 lecm 29988 pjmuli 30060 pjige0 30062 pjhfo 30077 pj11 30085 eigre 30206 eigorth 30209 hoddi 30361 nmlnop0 30369 lnopeq 30380 lnopunilem2 30382 nmbdoplb 30396 nmcopex 30400 nmcoplb 30401 lnopcon 30406 lnfn0 30418 lnfnmul 30419 nmcfnex 30424 nmcfnlb 30425 lnfncon 30427 riesz4 30435 riesz1 30436 cnlnadjeu 30449 pjhmop 30521 pjidmco 30552 mdslmd1lem3 30698 mdslmd1lem4 30699 csmdsymi 30705 hatomic 30731 atord 30759 atcvat2 30760 bnj941 32761 bnj944 32927 kur14 33187 abs2sqle 33647 abs2sqlt 33648 onsucconn 34636 onsucsuccmp 34642 sdclem1 35910 mnurnd 41908 bnd2d 46398 |
Copyright terms: Public domain | W3C validator |