Theorem elimel 4558

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

Syntax hints:   ∈ wcel 2143  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4489

This theorem is referenced by:  fprg  7154  orduninsuc  7840  oawordeu  8541  oeoa  8584  omopth  8649  unfilem3  9268  inar1  10761  supsr  11098  renegcl  11522  peano5uzti  12687  ltweuz  13999  uzenom  14002  seqfn  14051  seq1  14052  seqp1  14054  sqeqor  14254  binom2  14255  nn0opth2  14310  faclbnd4lem2  14332  hashxp  14473  dvdsle  16369  divalglem7  16458  divalg  16462  gcdaddm  16584  smadiadetr  22813  iblcnlem  25929  ax5seglem8  29267  elimnv  31016  elimnvu  31017  nmlno0i  31127  nmblolbi  31133  blocn  31140  elimphu  31154  ubth  31206  htth  31251  ifhvhv0  31355  normlem6  31448  norm-iii  31473  norm3lemt  31485  ifchhv  31577  hhssablo  31596  hhssnvt  31598  shscl  31651  shslej  31713  shincl  31714  omlsii  31736  pjoml  31769  pjoc2  31772  chm0  31824  chne0  31827  chocin  31828  chj0  31830  chlejb1  31845  chnle  31847  ledi  31873  h1datom  31915  cmbr3  31941  pjoml2  31944  cmcm  31947  cmcm3  31948  lecm  31950  pjmuli  32022  pjige0  32024  pjhfo  32039  pj11  32047  eigre  32168  eigorth  32171  hoddi  32323  nmlnop0  32331  lnopeq  32342  lnopunilem2  32344  nmbdoplb  32358  nmcopex  32362  nmcoplb  32363  lnopcon  32368  lnfn0  32380  lnfnmul  32381  nmcfnex  32386  nmcfnlb  32387  lnfncon  32389  riesz4  32397  riesz1  32398  cnlnadjeu  32411  pjhmop  32483  pjidmco  32514  mdslmd1lem3  32660  mdslmd1lem4  32661  csmdsymi  32667  hatomic  32693  atord  32721  atcvat2  32722  bnj941  35142  bnj944  35307  kur14  35689  abs2sqle  36153  abs2sqlt  36154  onsucconn  36930  onsucsuccmp  36936  sdclem1  38375  mnurnd  44976  bnd2d  50442