Theorem elimel 4536

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

Syntax hints:   ∈ wcel 2114  ifcif 4466

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  fprg  7109  orduninsuc  7794  oawordeu  8490  oeoa  8533  omopth  8598  unfilem3  9217  inar1  10698  supsr  11035  renegcl  11457  peano5uzti  12619  ltweuz  13923  uzenom  13926  seqfn  13975  seq1  13976  seqp1  13978  sqeqor  14178  binom2  14179  nn0opth2  14234  faclbnd4lem2  14256  hashxp  14396  dvdsle  16279  divalglem7  16368  divalg  16372  gcdaddm  16494  smadiadetr  22640  iblcnlem  25756  ax5seglem8  29005  elimnv  30754  elimnvu  30755  nmlno0i  30865  nmblolbi  30871  blocn  30878  elimphu  30892  ubth  30944  htth  30989  ifhvhv0  31093  normlem6  31186  norm-iii  31211  norm3lemt  31223  ifchhv  31315  hhssablo  31334  hhssnvt  31336  shscl  31389  shslej  31451  shincl  31452  omlsii  31474  pjoml  31507  pjoc2  31510  chm0  31562  chne0  31565  chocin  31566  chj0  31568  chlejb1  31583  chnle  31585  ledi  31611  h1datom  31653  cmbr3  31679  pjoml2  31682  cmcm  31685  cmcm3  31686  lecm  31688  pjmuli  31760  pjige0  31762  pjhfo  31777  pj11  31785  eigre  31906  eigorth  31909  hoddi  32061  nmlnop0  32069  lnopeq  32080  lnopunilem2  32082  nmbdoplb  32096  nmcopex  32100  nmcoplb  32101  lnopcon  32106  lnfn0  32118  lnfnmul  32119  nmcfnex  32124  nmcfnlb  32125  lnfncon  32127  riesz4  32135  riesz1  32136  cnlnadjeu  32149  pjhmop  32221  pjidmco  32252  mdslmd1lem3  32398  mdslmd1lem4  32399  csmdsymi  32405  hatomic  32431  atord  32459  atcvat2  32460  bnj941  34915  bnj944  35080  kur14  35398  abs2sqle  35862  abs2sqlt  35863  onsucconn  36620  onsucsuccmp  36626  sdclem1  38064  mnurnd  44710  bnd2d  50156