Theorem elimel 4555

Description: Eliminate a membership hypothesis for weak deduction theorem, when special case 𝐵 ∈ 𝐶 is provable. (Contributed by NM, 15-May-1999.)

Hypothesis

Ref	Expression
elimel.1	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
elimel	⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶

Proof of Theorem elimel

Step	Hyp	Ref	Expression
1		eleq1 2850	. 2 ⊢ (𝐴 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶))
2		eleq1 2850	. 2 ⊢ (𝐵 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶))
3		elimel.1	. 2 ⊢ 𝐵 ∈ 𝐶
4	1, 2, 3	elimhyp 4551	1 ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶

This proof depends on syntax axioms:   ∈ wcel 2145  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4486

This theorem is used by:  fprg  7156  orduninsuc  7843  oawordeu  8546  oeoa  8589  omopth  8654  unfilem3  9281  inar1  10788  supsr  11125  renegcl  11549  peano5uzti  12715  ltweuz  14029  uzenom  14032  seqfn  14081  seq1  14082  seqp1  14084  sqeqor  14284  binom2  14285  nn0opth2  14340  faclbnd4lem2  14362  hashxp  14503  dvdsle  16406  divalglem7  16495  divalg  16499  gcdaddm  16621  smadiadetr  22903  iblcnlem  26023  ax5seglem8  29401  elimnv  31172  elimnvu  31173  nmlno0i  31283  nmblolbi  31289  blocn  31296  elimphu  31310  ubth  31362  htth  31407  ifhvhv0  31511  normlem6  31604  norm-iii  31629  norm3lemt  31641  ifchhv  31733  hhssablo  31752  hhssnvt  31754  shscl  31807  shslej  31869  shincl  31870  omlsii  31892  pjoml  31925  pjoc2  31928  chm0  31980  chne0  31983  chocin  31984  chj0  31986  chlejb1  32001  chnle  32003  ledi  32029  h1datom  32071  cmbr3  32097  pjoml2  32100  cmcm  32103  cmcm3  32104  lecm  32106  pjmuli  32178  pjige0  32180  pjhfo  32195  pj11  32203  eigre  32324  eigorth  32327  hoddi  32479  nmlnop0  32487  lnopeq  32498  lnopunilem2  32500  nmbdoplb  32514  nmcopex  32518  nmcoplb  32519  lnopcon  32524  lnfn0  32536  lnfnmul  32537  nmcfnex  32542  nmcfnlb  32543  lnfncon  32545  riesz4  32553  riesz1  32554  cnlnadjeu  32567  pjhmop  32639  pjidmco  32670  mdslmd1lem3  32816  mdslmd1lem4  32817  csmdsymi  32823  hatomic  32849  atord  32877  atcvat2  32878  bnj941  35290  bnj944  35455  kur14  35803  abs2sqle  36267  abs2sqlt  36268  onsucconn  37065  onsucsuccmp  37071  sdclem1  38501  mnurnd  45115  bnd2d  50615