Theorem elimel 4537

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

Syntax hints:   ∈ wcel 2114  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  fprg  7100  orduninsuc  7785  oawordeu  8481  oeoa  8524  omopth  8589  unfilem3  9208  inar1  10687  supsr  11024  renegcl  11446  peano5uzti  12608  ltweuz  13912  uzenom  13915  seqfn  13964  seq1  13965  seqp1  13967  sqeqor  14167  binom2  14168  nn0opth2  14223  faclbnd4lem2  14245  hashxp  14385  dvdsle  16268  divalglem7  16357  divalg  16361  gcdaddm  16483  smadiadetr  22649  iblcnlem  25765  ax5seglem8  29024  elimnv  30774  elimnvu  30775  nmlno0i  30885  nmblolbi  30891  blocn  30898  elimphu  30912  ubth  30964  htth  31009  ifhvhv0  31113  normlem6  31206  norm-iii  31231  norm3lemt  31243  ifchhv  31335  hhssablo  31354  hhssnvt  31356  shscl  31409  shslej  31471  shincl  31472  omlsii  31494  pjoml  31527  pjoc2  31530  chm0  31582  chne0  31585  chocin  31586  chj0  31588  chlejb1  31603  chnle  31605  ledi  31631  h1datom  31673  cmbr3  31699  pjoml2  31702  cmcm  31705  cmcm3  31706  lecm  31708  pjmuli  31780  pjige0  31782  pjhfo  31797  pj11  31805  eigre  31926  eigorth  31929  hoddi  32081  nmlnop0  32089  lnopeq  32100  lnopunilem2  32102  nmbdoplb  32116  nmcopex  32120  nmcoplb  32121  lnopcon  32126  lnfn0  32138  lnfnmul  32139  nmcfnex  32144  nmcfnlb  32145  lnfncon  32147  riesz4  32155  riesz1  32156  cnlnadjeu  32169  pjhmop  32241  pjidmco  32272  mdslmd1lem3  32418  mdslmd1lem4  32419  csmdsymi  32425  hatomic  32451  atord  32479  atcvat2  32480  bnj941  34936  bnj944  35101  kur14  35419  abs2sqle  35883  abs2sqlt  35884  onsucconn  36641  onsucsuccmp  36647  sdclem1  38075  mnurnd  44725  bnd2d  50153