![]() |
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 2825 | . 2 ⊢ (𝐴 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶)) | |
2 | eleq1 2825 | . 2 ⊢ (𝐵 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶)) | |
3 | elimel.1 | . 2 ⊢ 𝐵 ∈ 𝐶 | |
4 | 1, 2, 3 | elimhyp 4551 | 1 ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 ifcif 4486 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-if 4487 |
This theorem is referenced by: fprg 7101 orduninsuc 7779 oawordeu 8502 oeoa 8544 omopth 8608 unfilem3 9256 inar1 10711 supsr 11048 renegcl 11464 peano5uzti 12593 eluzaddOLD 12798 eluzsubOLD 12799 ltweuz 13866 uzenom 13869 seqfn 13918 seq1 13919 seqp1 13921 sqeqor 14120 binom2 14121 nn0opth2 14172 faclbnd4lem2 14194 hashxp 14334 dvdsle 16192 divalglem7 16281 divalg 16285 gcdaddm 16405 smadiadetr 22024 iblcnlem 25153 ax5seglem8 27885 elimnv 29625 elimnvu 29626 nmlno0i 29736 nmblolbi 29742 blocn 29749 elimphu 29763 ubth 29815 htth 29860 ifhvhv0 29964 normlem6 30057 norm-iii 30082 norm3lemt 30094 ifchhv 30186 hhssablo 30205 hhssnvt 30207 shscl 30260 shslej 30322 shincl 30323 omlsii 30345 pjoml 30378 pjoc2 30381 chm0 30433 chne0 30436 chocin 30437 chj0 30439 chlejb1 30454 chnle 30456 ledi 30482 h1datom 30524 cmbr3 30550 pjoml2 30553 cmcm 30556 cmcm3 30557 lecm 30559 pjmuli 30631 pjige0 30633 pjhfo 30648 pj11 30656 eigre 30777 eigorth 30780 hoddi 30932 nmlnop0 30940 lnopeq 30951 lnopunilem2 30953 nmbdoplb 30967 nmcopex 30971 nmcoplb 30972 lnopcon 30977 lnfn0 30989 lnfnmul 30990 nmcfnex 30995 nmcfnlb 30996 lnfncon 30998 riesz4 31006 riesz1 31007 cnlnadjeu 31020 pjhmop 31092 pjidmco 31123 mdslmd1lem3 31269 mdslmd1lem4 31270 csmdsymi 31276 hatomic 31302 atord 31330 atcvat2 31331 bnj941 33384 bnj944 33550 kur14 33810 abs2sqle 34268 abs2sqlt 34269 onsucconn 34910 onsucsuccmp 34916 sdclem1 36202 mnurnd 42553 bnd2d 47116 |
Copyright terms: Public domain | W3C validator |