Theorem elimel 4127

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

Syntax hints:   ∈ wcel 1992  ifcif 4063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-if 4064

This theorem is referenced by:  fprg  6377  orduninsuc  6991  oawordeu  7581  oeoa  7623  omopth  7684  unfilem3  8171  inar1  9542  supsr  9878  renegcl  10289  peano5uzti  11411  eluzadd  11660  eluzsub  11661  ltweuz  12697  uzenom  12700  seqfn  12750  seq1  12751  seqp1  12753  sqeqor  12915  binom2  12916  nn0opth2  12996  faclbnd4lem2  13018  hashxp  13158  dvdsle  14951  divalglem7  15041  divalg  15045  gcdaddm  15165  smadiadetr  20395  iblcnlem  23456  ax5seglem8  25711  elimnv  27378  elimnvu  27379  nmlno0i  27489  nmblolbi  27495  blocn  27502  elimphu  27516  ubth  27569  htth  27615  ifhvhv0  27719  normlem6  27812  norm-iii  27837  norm3lemt  27849  ifchhv  27941  hhssablo  27960  hhssnvt  27962  shscl  28017  shslej  28079  shincl  28080  omlsii  28102  pjoml  28135  pjoc2  28138  chm0  28190  chne0  28193  chocin  28194  chj0  28196  chlejb1  28211  chnle  28213  ledi  28239  h1datom  28281  cmbr3  28307  pjoml2  28310  cmcm  28313  cmcm3  28314  lecm  28316  pjmuli  28388  pjige0  28390  pjhfo  28405  pj11  28413  eigre  28534  eigorth  28537  hoddi  28689  nmlnop0  28697  lnopeq  28708  lnopunilem2  28710  nmbdoplb  28724  nmcopex  28728  nmcoplb  28729  lnopcon  28734  lnfn0  28746  lnfnmul  28747  nmcfnex  28752  nmcfnlb  28753  lnfncon  28755  riesz4  28763  riesz1  28764  cnlnadjeu  28777  pjhmop  28849  pjidmco  28880  mdslmd1lem3  29026  mdslmd1lem4  29027  csmdsymi  29033  hatomic  29059  atord  29087  atcvat2  29088  bnj941  30543  bnj944  30708  kur14  30898  abs2sqle  31274  abs2sqlt  31275  onsucconn  32071  onsucsuccmp  32077  sdclem1  33157  bnd2d  41694