Theorem elimel 4600

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

Syntax hints:   ∈ wcel 2106  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-if 4532

This theorem is referenced by:  fprg  7175  orduninsuc  7864  oawordeu  8592  oeoa  8634  omopth  8699  unfilem3  9343  inar1  10813  supsr  11150  renegcl  11570  peano5uzti  12706  eluzaddOLD  12911  eluzsubOLD  12912  ltweuz  13999  uzenom  14002  seqfn  14051  seq1  14052  seqp1  14054  sqeqor  14252  binom2  14253  nn0opth2  14308  faclbnd4lem2  14330  hashxp  14470  dvdsle  16344  divalglem7  16433  divalg  16437  gcdaddm  16559  smadiadetr  22697  iblcnlem  25839  ax5seglem8  28966  elimnv  30712  elimnvu  30713  nmlno0i  30823  nmblolbi  30829  blocn  30836  elimphu  30850  ubth  30902  htth  30947  ifhvhv0  31051  normlem6  31144  norm-iii  31169  norm3lemt  31181  ifchhv  31273  hhssablo  31292  hhssnvt  31294  shscl  31347  shslej  31409  shincl  31410  omlsii  31432  pjoml  31465  pjoc2  31468  chm0  31520  chne0  31523  chocin  31524  chj0  31526  chlejb1  31541  chnle  31543  ledi  31569  h1datom  31611  cmbr3  31637  pjoml2  31640  cmcm  31643  cmcm3  31644  lecm  31646  pjmuli  31718  pjige0  31720  pjhfo  31735  pj11  31743  eigre  31864  eigorth  31867  hoddi  32019  nmlnop0  32027  lnopeq  32038  lnopunilem2  32040  nmbdoplb  32054  nmcopex  32058  nmcoplb  32059  lnopcon  32064  lnfn0  32076  lnfnmul  32077  nmcfnex  32082  nmcfnlb  32083  lnfncon  32085  riesz4  32093  riesz1  32094  cnlnadjeu  32107  pjhmop  32179  pjidmco  32210  mdslmd1lem3  32356  mdslmd1lem4  32357  csmdsymi  32363  hatomic  32389  atord  32417  atcvat2  32418  bnj941  34765  bnj944  34931  kur14  35201  abs2sqle  35665  abs2sqlt  35666  onsucconn  36421  onsucsuccmp  36427  sdclem1  37730  mnurnd  44279  bnd2d  48912