Theorem elimel 4553

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

Syntax hints:   ∈ wcel 2145  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4484

This theorem is referenced by:  fprg  7142  orduninsuc  7827  oawordeu  8528  oeoa  8571  omopth  8636  unfilem3  9255  inar1  10748  supsr  11085  renegcl  11509  peano5uzti  12674  ltweuz  13985  uzenom  13988  seqfn  14037  seq1  14038  seqp1  14040  sqeqor  14240  binom2  14241  nn0opth2  14296  faclbnd4lem2  14318  hashxp  14459  dvdsle  16356  divalglem7  16445  divalg  16449  gcdaddm  16571  smadiadetr  22789  iblcnlem  25905  ax5seglem8  29191  elimnv  30940  elimnvu  30941  nmlno0i  31051  nmblolbi  31057  blocn  31064  elimphu  31078  ubth  31130  htth  31175  ifhvhv0  31279  normlem6  31372  norm-iii  31397  norm3lemt  31409  ifchhv  31501  hhssablo  31520  hhssnvt  31522  shscl  31575  shslej  31637  shincl  31638  omlsii  31660  pjoml  31693  pjoc2  31696  chm0  31748  chne0  31751  chocin  31752  chj0  31754  chlejb1  31769  chnle  31771  ledi  31797  h1datom  31839  cmbr3  31865  pjoml2  31868  cmcm  31871  cmcm3  31872  lecm  31874  pjmuli  31946  pjige0  31948  pjhfo  31963  pj11  31971  eigre  32092  eigorth  32095  hoddi  32247  nmlnop0  32255  lnopeq  32266  lnopunilem2  32268  nmbdoplb  32282  nmcopex  32286  nmcoplb  32287  lnopcon  32292  lnfn0  32304  lnfnmul  32305  nmcfnex  32310  nmcfnlb  32311  lnfncon  32313  riesz4  32321  riesz1  32322  cnlnadjeu  32335  pjhmop  32407  pjidmco  32438  mdslmd1lem3  32584  mdslmd1lem4  32585  csmdsymi  32591  hatomic  32617  atord  32645  atcvat2  32646  bnj941  35073  bnj944  35238  kur14  35574  abs2sqle  36038  abs2sqlt  36039  onsucconn  36806  onsucsuccmp  36812  sdclem1  38249  mnurnd  44852  bnd2d  50311