Theorem elimel 4597

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

Syntax hints:   ∈ wcel 2106  ifcif 4528

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-if 4529

This theorem is referenced by:  fprg  7152  orduninsuc  7831  oawordeu  8554  oeoa  8596  omopth  8660  unfilem3  9311  inar1  10769  supsr  11106  renegcl  11522  peano5uzti  12651  eluzaddOLD  12856  eluzsubOLD  12857  ltweuz  13925  uzenom  13928  seqfn  13977  seq1  13978  seqp1  13980  sqeqor  14179  binom2  14180  nn0opth2  14231  faclbnd4lem2  14253  hashxp  14393  dvdsle  16252  divalglem7  16341  divalg  16345  gcdaddm  16465  smadiadetr  22176  iblcnlem  25305  ax5seglem8  28191  elimnv  29931  elimnvu  29932  nmlno0i  30042  nmblolbi  30048  blocn  30055  elimphu  30069  ubth  30121  htth  30166  ifhvhv0  30270  normlem6  30363  norm-iii  30388  norm3lemt  30400  ifchhv  30492  hhssablo  30511  hhssnvt  30513  shscl  30566  shslej  30628  shincl  30629  omlsii  30651  pjoml  30684  pjoc2  30687  chm0  30739  chne0  30742  chocin  30743  chj0  30745  chlejb1  30760  chnle  30762  ledi  30788  h1datom  30830  cmbr3  30856  pjoml2  30859  cmcm  30862  cmcm3  30863  lecm  30865  pjmuli  30937  pjige0  30939  pjhfo  30954  pj11  30962  eigre  31083  eigorth  31086  hoddi  31238  nmlnop0  31246  lnopeq  31257  lnopunilem2  31259  nmbdoplb  31273  nmcopex  31277  nmcoplb  31278  lnopcon  31283  lnfn0  31295  lnfnmul  31296  nmcfnex  31301  nmcfnlb  31302  lnfncon  31304  riesz4  31312  riesz1  31313  cnlnadjeu  31326  pjhmop  31398  pjidmco  31429  mdslmd1lem3  31575  mdslmd1lem4  31576  csmdsymi  31582  hatomic  31608  atord  31636  atcvat2  31637  bnj941  33778  bnj944  33944  kur14  34202  abs2sqle  34660  abs2sqlt  34661  onsucconn  35318  onsucsuccmp  35324  sdclem1  36606  mnurnd  43032  bnd2d  47716