Theorem elimel 4594

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 4590	1 ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶

Syntax hints:   ∈ wcel 2107  ifcif 4524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-if 4525

This theorem is referenced by:  fprg  7174  orduninsuc  7865  oawordeu  8594  oeoa  8636  omopth  8701  unfilem3  9346  inar1  10816  supsr  11153  renegcl  11573  peano5uzti  12710  eluzaddOLD  12914  eluzsubOLD  12915  ltweuz  14003  uzenom  14006  seqfn  14055  seq1  14056  seqp1  14058  sqeqor  14256  binom2  14257  nn0opth2  14312  faclbnd4lem2  14334  hashxp  14474  dvdsle  16348  divalglem7  16437  divalg  16441  gcdaddm  16563  smadiadetr  22682  iblcnlem  25825  ax5seglem8  28952  elimnv  30703  elimnvu  30704  nmlno0i  30814  nmblolbi  30820  blocn  30827  elimphu  30841  ubth  30893  htth  30938  ifhvhv0  31042  normlem6  31135  norm-iii  31160  norm3lemt  31172  ifchhv  31264  hhssablo  31283  hhssnvt  31285  shscl  31338  shslej  31400  shincl  31401  omlsii  31423  pjoml  31456  pjoc2  31459  chm0  31511  chne0  31514  chocin  31515  chj0  31517  chlejb1  31532  chnle  31534  ledi  31560  h1datom  31602  cmbr3  31628  pjoml2  31631  cmcm  31634  cmcm3  31635  lecm  31637  pjmuli  31709  pjige0  31711  pjhfo  31726  pj11  31734  eigre  31855  eigorth  31858  hoddi  32010  nmlnop0  32018  lnopeq  32029  lnopunilem2  32031  nmbdoplb  32045  nmcopex  32049  nmcoplb  32050  lnopcon  32055  lnfn0  32067  lnfnmul  32068  nmcfnex  32073  nmcfnlb  32074  lnfncon  32076  riesz4  32084  riesz1  32085  cnlnadjeu  32098  pjhmop  32170  pjidmco  32201  mdslmd1lem3  32347  mdslmd1lem4  32348  csmdsymi  32354  hatomic  32380  atord  32408  atcvat2  32409  bnj941  34787  bnj944  34953  kur14  35222  abs2sqle  35686  abs2sqlt  35687  onsucconn  36440  onsucsuccmp  36446  sdclem1  37751  mnurnd  44307  bnd2d  49255