Theorem elimel 4548

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

Syntax hints:   ∈ wcel 2109  ifcif 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4479

This theorem is referenced by:  fprg  7093  orduninsuc  7783  oawordeu  8480  oeoa  8522  omopth  8587  unfilem3  9214  inar1  10688  supsr  11025  renegcl  11445  peano5uzti  12584  eluzaddOLD  12788  eluzsubOLD  12789  ltweuz  13886  uzenom  13889  seqfn  13938  seq1  13939  seqp1  13941  sqeqor  14141  binom2  14142  nn0opth2  14197  faclbnd4lem2  14219  hashxp  14359  dvdsle  16239  divalglem7  16328  divalg  16332  gcdaddm  16454  smadiadetr  22578  iblcnlem  25706  ax5seglem8  28899  elimnv  30645  elimnvu  30646  nmlno0i  30756  nmblolbi  30762  blocn  30769  elimphu  30783  ubth  30835  htth  30880  ifhvhv0  30984  normlem6  31077  norm-iii  31102  norm3lemt  31114  ifchhv  31206  hhssablo  31225  hhssnvt  31227  shscl  31280  shslej  31342  shincl  31343  omlsii  31365  pjoml  31398  pjoc2  31401  chm0  31453  chne0  31456  chocin  31457  chj0  31459  chlejb1  31474  chnle  31476  ledi  31502  h1datom  31544  cmbr3  31570  pjoml2  31573  cmcm  31576  cmcm3  31577  lecm  31579  pjmuli  31651  pjige0  31653  pjhfo  31668  pj11  31676  eigre  31797  eigorth  31800  hoddi  31952  nmlnop0  31960  lnopeq  31971  lnopunilem2  31973  nmbdoplb  31987  nmcopex  31991  nmcoplb  31992  lnopcon  31997  lnfn0  32009  lnfnmul  32010  nmcfnex  32015  nmcfnlb  32016  lnfncon  32018  riesz4  32026  riesz1  32027  cnlnadjeu  32040  pjhmop  32112  pjidmco  32143  mdslmd1lem3  32289  mdslmd1lem4  32290  csmdsymi  32296  hatomic  32322  atord  32350  atcvat2  32351  bnj941  34741  bnj944  34907  kur14  35191  abs2sqle  35655  abs2sqlt  35656  onsucconn  36414  onsucsuccmp  36420  sdclem1  37725  mnurnd  44259  bnd2d  49670