Theorem elimel 4549

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

Syntax hints:   ∈ wcel 2113  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480

This theorem is referenced by:  fprg  7100  orduninsuc  7785  oawordeu  8482  oeoa  8525  omopth  8590  unfilem3  9207  inar1  10686  supsr  11023  renegcl  11444  peano5uzti  12582  ltweuz  13884  uzenom  13887  seqfn  13936  seq1  13937  seqp1  13939  sqeqor  14139  binom2  14140  nn0opth2  14195  faclbnd4lem2  14217  hashxp  14357  dvdsle  16237  divalglem7  16326  divalg  16330  gcdaddm  16452  smadiadetr  22619  iblcnlem  25746  ax5seglem8  29009  elimnv  30758  elimnvu  30759  nmlno0i  30869  nmblolbi  30875  blocn  30882  elimphu  30896  ubth  30948  htth  30993  ifhvhv0  31097  normlem6  31190  norm-iii  31215  norm3lemt  31227  ifchhv  31319  hhssablo  31338  hhssnvt  31340  shscl  31393  shslej  31455  shincl  31456  omlsii  31478  pjoml  31511  pjoc2  31514  chm0  31566  chne0  31569  chocin  31570  chj0  31572  chlejb1  31587  chnle  31589  ledi  31615  h1datom  31657  cmbr3  31683  pjoml2  31686  cmcm  31689  cmcm3  31690  lecm  31692  pjmuli  31764  pjige0  31766  pjhfo  31781  pj11  31789  eigre  31910  eigorth  31913  hoddi  32065  nmlnop0  32073  lnopeq  32084  lnopunilem2  32086  nmbdoplb  32100  nmcopex  32104  nmcoplb  32105  lnopcon  32110  lnfn0  32122  lnfnmul  32123  nmcfnex  32128  nmcfnlb  32129  lnfncon  32131  riesz4  32139  riesz1  32140  cnlnadjeu  32153  pjhmop  32225  pjidmco  32256  mdslmd1lem3  32402  mdslmd1lem4  32403  csmdsymi  32409  hatomic  32435  atord  32463  atcvat2  32464  bnj941  34928  bnj944  35094  kur14  35410  abs2sqle  35874  abs2sqlt  35875  onsucconn  36632  onsucsuccmp  36638  sdclem1  37940  mnurnd  44520  bnd2d  49922