Theorem elimel 4492

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

Syntax hints:   ∈ wcel 2111  ifcif 4425

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4426

This theorem is referenced by:  fprg  6894  orduninsuc  7538  oawordeu  8164  oeoa  8206  omopth  8268  unfilem3  8768  inar1  10186  supsr  10523  renegcl  10938  peano5uzti  12060  eluzadd  12261  eluzsub  12262  ltweuz  13324  uzenom  13327  seqfn  13376  seq1  13377  seqp1  13379  sqeqor  13574  binom2  13575  nn0opth2  13628  faclbnd4lem2  13650  hashxp  13791  dvdsle  15652  divalglem7  15740  divalg  15744  gcdaddm  15863  smadiadetr  21280  iblcnlem  24392  ax5seglem8  26730  elimnv  28466  elimnvu  28467  nmlno0i  28577  nmblolbi  28583  blocn  28590  elimphu  28604  ubth  28656  htth  28701  ifhvhv0  28805  normlem6  28898  norm-iii  28923  norm3lemt  28935  ifchhv  29027  hhssablo  29046  hhssnvt  29048  shscl  29101  shslej  29163  shincl  29164  omlsii  29186  pjoml  29219  pjoc2  29222  chm0  29274  chne0  29277  chocin  29278  chj0  29280  chlejb1  29295  chnle  29297  ledi  29323  h1datom  29365  cmbr3  29391  pjoml2  29394  cmcm  29397  cmcm3  29398  lecm  29400  pjmuli  29472  pjige0  29474  pjhfo  29489  pj11  29497  eigre  29618  eigorth  29621  hoddi  29773  nmlnop0  29781  lnopeq  29792  lnopunilem2  29794  nmbdoplb  29808  nmcopex  29812  nmcoplb  29813  lnopcon  29818  lnfn0  29830  lnfnmul  29831  nmcfnex  29836  nmcfnlb  29837  lnfncon  29839  riesz4  29847  riesz1  29848  cnlnadjeu  29861  pjhmop  29933  pjidmco  29964  mdslmd1lem3  30110  mdslmd1lem4  30111  csmdsymi  30117  hatomic  30143  atord  30171  atcvat2  30172  bnj941  32154  bnj944  32320  kur14  32576  abs2sqle  33036  abs2sqlt  33037  onsucconn  33899  onsucsuccmp  33905  sdclem1  35181  mnurnd  40991  bnd2d  45211