Theorem elimel 4562

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

This proof depends on syntax axioms:   ∈ wcel 2146  ifcif 4492

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-if 4493

This theorem is used by:  fprg  7159  orduninsuc  7848  oawordeu  8549  oeoa  8592  omopth  8657  unfilem3  9277  inar1  10778  supsr  11115  renegcl  11539  peano5uzti  12704  ltweuz  14017  uzenom  14020  seqfn  14069  seq1  14070  seqp1  14072  sqeqor  14272  binom2  14273  nn0opth2  14328  faclbnd4lem2  14350  hashxp  14491  dvdsle  16393  divalglem7  16482  divalg  16486  gcdaddm  16608  smadiadetr  22869  iblcnlem  25985  ax5seglem8  29323  elimnv  31072  elimnvu  31073  nmlno0i  31183  nmblolbi  31189  blocn  31196  elimphu  31210  ubth  31262  htth  31307  ifhvhv0  31411  normlem6  31504  norm-iii  31529  norm3lemt  31541  ifchhv  31633  hhssablo  31652  hhssnvt  31654  shscl  31707  shslej  31769  shincl  31770  omlsii  31792  pjoml  31825  pjoc2  31828  chm0  31880  chne0  31883  chocin  31884  chj0  31886  chlejb1  31901  chnle  31903  ledi  31929  h1datom  31971  cmbr3  31997  pjoml2  32000  cmcm  32003  cmcm3  32004  lecm  32006  pjmuli  32078  pjige0  32080  pjhfo  32095  pj11  32103  eigre  32224  eigorth  32227  hoddi  32379  nmlnop0  32387  lnopeq  32398  lnopunilem2  32400  nmbdoplb  32414  nmcopex  32418  nmcoplb  32419  lnopcon  32424  lnfn0  32436  lnfnmul  32437  nmcfnex  32442  nmcfnlb  32443  lnfncon  32445  riesz4  32453  riesz1  32454  cnlnadjeu  32467  pjhmop  32539  pjidmco  32570  mdslmd1lem3  32716  mdslmd1lem4  32717  csmdsymi  32723  hatomic  32749  atord  32777  atcvat2  32778  bnj941  35193  bnj944  35358  kur14  35729  abs2sqle  36193  abs2sqlt  36194  onsucconn  36990  onsucsuccmp  36996  sdclem1  38435  mnurnd  45034  bnd2d  50500