Theorem elimel 4525

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 2826	. 2 ⊢ (𝐴 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶))
2		eleq1 2826	. 2 ⊢ (𝐵 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶))
3		elimel.1	. 2 ⊢ 𝐵 ∈ 𝐶
4	1, 2, 3	elimhyp 4521	1 ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶

Syntax hints:   ∈ wcel 2108  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  fprg  7009  orduninsuc  7665  oawordeu  8348  oeoa  8390  omopth  8452  unfilem3  9010  inar1  10462  supsr  10799  renegcl  11214  peano5uzti  12340  eluzadd  12542  eluzsub  12543  ltweuz  13609  uzenom  13612  seqfn  13661  seq1  13662  seqp1  13664  sqeqor  13860  binom2  13861  nn0opth2  13914  faclbnd4lem2  13936  hashxp  14077  dvdsle  15947  divalglem7  16036  divalg  16040  gcdaddm  16160  smadiadetr  21732  iblcnlem  24858  ax5seglem8  27207  elimnv  28946  elimnvu  28947  nmlno0i  29057  nmblolbi  29063  blocn  29070  elimphu  29084  ubth  29136  htth  29181  ifhvhv0  29285  normlem6  29378  norm-iii  29403  norm3lemt  29415  ifchhv  29507  hhssablo  29526  hhssnvt  29528  shscl  29581  shslej  29643  shincl  29644  omlsii  29666  pjoml  29699  pjoc2  29702  chm0  29754  chne0  29757  chocin  29758  chj0  29760  chlejb1  29775  chnle  29777  ledi  29803  h1datom  29845  cmbr3  29871  pjoml2  29874  cmcm  29877  cmcm3  29878  lecm  29880  pjmuli  29952  pjige0  29954  pjhfo  29969  pj11  29977  eigre  30098  eigorth  30101  hoddi  30253  nmlnop0  30261  lnopeq  30272  lnopunilem2  30274  nmbdoplb  30288  nmcopex  30292  nmcoplb  30293  lnopcon  30298  lnfn0  30310  lnfnmul  30311  nmcfnex  30316  nmcfnlb  30317  lnfncon  30319  riesz4  30327  riesz1  30328  cnlnadjeu  30341  pjhmop  30413  pjidmco  30444  mdslmd1lem3  30590  mdslmd1lem4  30591  csmdsymi  30597  hatomic  30623  atord  30651  atcvat2  30652  bnj941  32652  bnj944  32818  kur14  33078  abs2sqle  33538  abs2sqlt  33539  onsucconn  34554  onsucsuccmp  34560  sdclem1  35828  mnurnd  41790  bnd2d  46273