Theorem elimel 4575

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

Syntax hints:   ∈ wcel 2109  ifcif 4505

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-if 4506

This theorem is referenced by:  fprg  7150  orduninsuc  7843  oawordeu  8572  oeoa  8614  omopth  8679  unfilem3  9322  inar1  10794  supsr  11131  renegcl  11551  peano5uzti  12688  eluzaddOLD  12892  eluzsubOLD  12893  ltweuz  13984  uzenom  13987  seqfn  14036  seq1  14037  seqp1  14039  sqeqor  14239  binom2  14240  nn0opth2  14295  faclbnd4lem2  14317  hashxp  14457  dvdsle  16334  divalglem7  16423  divalg  16427  gcdaddm  16549  smadiadetr  22618  iblcnlem  25747  ax5seglem8  28920  elimnv  30669  elimnvu  30670  nmlno0i  30780  nmblolbi  30786  blocn  30793  elimphu  30807  ubth  30859  htth  30904  ifhvhv0  31008  normlem6  31101  norm-iii  31126  norm3lemt  31138  ifchhv  31230  hhssablo  31249  hhssnvt  31251  shscl  31304  shslej  31366  shincl  31367  omlsii  31389  pjoml  31422  pjoc2  31425  chm0  31477  chne0  31480  chocin  31481  chj0  31483  chlejb1  31498  chnle  31500  ledi  31526  h1datom  31568  cmbr3  31594  pjoml2  31597  cmcm  31600  cmcm3  31601  lecm  31603  pjmuli  31675  pjige0  31677  pjhfo  31692  pj11  31700  eigre  31821  eigorth  31824  hoddi  31976  nmlnop0  31984  lnopeq  31995  lnopunilem2  31997  nmbdoplb  32011  nmcopex  32015  nmcoplb  32016  lnopcon  32021  lnfn0  32033  lnfnmul  32034  nmcfnex  32039  nmcfnlb  32040  lnfncon  32042  riesz4  32050  riesz1  32051  cnlnadjeu  32064  pjhmop  32136  pjidmco  32167  mdslmd1lem3  32313  mdslmd1lem4  32314  csmdsymi  32320  hatomic  32346  atord  32374  atcvat2  32375  bnj941  34808  bnj944  34974  kur14  35243  abs2sqle  35707  abs2sqlt  35708  onsucconn  36461  onsucsuccmp  36467  sdclem1  37772  mnurnd  44282  bnd2d  49525