Theorem elimel 4531

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

Syntax hints:   ∈ wcel 2119  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-if 4462

This theorem is referenced by:  fprg  7105  orduninsuc  7790  oawordeu  8487  oeoa  8530  omopth  8595  unfilem3  9214  inar1  10696  supsr  11033  renegcl  11455  peano5uzti  12617  ltweuz  13921  uzenom  13924  seqfn  13973  seq1  13974  seqp1  13976  sqeqor  14176  binom2  14177  nn0opth2  14232  faclbnd4lem2  14254  hashxp  14394  dvdsle  16277  divalglem7  16366  divalg  16370  gcdaddm  16492  smadiadetr  22665  iblcnlem  25781  ax5seglem8  29030  elimnv  30779  elimnvu  30780  nmlno0i  30890  nmblolbi  30896  blocn  30903  elimphu  30917  ubth  30969  htth  31014  ifhvhv0  31118  normlem6  31211  norm-iii  31236  norm3lemt  31248  ifchhv  31340  hhssablo  31359  hhssnvt  31361  shscl  31414  shslej  31476  shincl  31477  omlsii  31499  pjoml  31532  pjoc2  31535  chm0  31587  chne0  31590  chocin  31591  chj0  31593  chlejb1  31608  chnle  31610  ledi  31636  h1datom  31678  cmbr3  31704  pjoml2  31707  cmcm  31710  cmcm3  31711  lecm  31713  pjmuli  31785  pjige0  31787  pjhfo  31802  pj11  31810  eigre  31931  eigorth  31934  hoddi  32086  nmlnop0  32094  lnopeq  32105  lnopunilem2  32107  nmbdoplb  32121  nmcopex  32125  nmcoplb  32126  lnopcon  32131  lnfn0  32143  lnfnmul  32144  nmcfnex  32149  nmcfnlb  32150  lnfncon  32152  riesz4  32160  riesz1  32161  cnlnadjeu  32174  pjhmop  32246  pjidmco  32277  mdslmd1lem3  32423  mdslmd1lem4  32424  csmdsymi  32430  hatomic  32456  atord  32484  atcvat2  32485  bnj941  34962  bnj944  35127  kur14  35451  abs2sqle  35915  abs2sqlt  35916  onsucconn  36673  onsucsuccmp  36679  sdclem1  38117  mnurnd  44734  bnd2d  50178