Theorem elimel 4552

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  fprg  7151  orduninsuc  7843  oawordeu  8547  oeoa  8590  omopth  8655  unfilem3  9283  bnd2d  9949  inar1  10841  supsr  11178  renegcl  11602  peano5uzti  12770  ltweuz  14084  uzenom  14087  seqfn  14136  seq1  14137  seqp1  14139  sqeqor  14340  binom2  14341  nn0opth2  14396  faclbnd4lem2  14418  hashxp  14559  dvdsle  16460  divalglem7  16549  divalg  16553  gcdaddm  16677  smadiadetr  22970  iblcnlem  26089  ax5seglem8  29496  elimnv  31267  elimnvu  31268  nmlno0i  31378  nmblolbi  31384  blocn  31391  elimphu  31405  ubth  31457  htth  31502  ifhvhv0  31606  normlem6  31699  norm-iii  31724  norm3lemt  31736  ifchhv  31828  hhssablo  31847  hhssnvt  31849  shscl  31902  shslej  31964  shincl  31965  omlsii  31987  pjoml  32020  pjoc2  32023  chm0  32075  chne0  32078  chocin  32079  chj0  32081  chlejb1  32096  chnle  32098  ledi  32124  h1datom  32166  cmbr3  32192  pjoml2  32195  cmcm  32198  cmcm3  32199  lecm  32201  pjmuli  32273  pjige0  32275  pjhfo  32290  pj11  32298  eigre  32419  eigorth  32422  hoddi  32574  nmlnop0  32582  lnopeq  32593  lnopunilem2  32595  nmbdoplb  32609  nmcopex  32613  nmcoplb  32614  lnopcon  32619  lnfn0  32631  lnfnmul  32632  nmcfnex  32637  nmcfnlb  32638  lnfncon  32640  riesz4  32648  riesz1  32649  cnlnadjeu  32662  pjhmop  32734  pjidmco  32765  mdslmd1lem3  32911  mdslmd1lem4  32912  csmdsymi  32918  hatomic  32944  atord  32972  atcvat2  32973  bnj941  35386  bnj944  35551  kur14  35950  abs2sqle  36414  abs2sqlt  36415  onsucconn  37196  onsucsuccmp  37202  sdclem1  38645  mnurnd  45226