Theorem elimel 1793

Description: Eliminate a membership hypothesis for weak deduction theorem, when special case B ∈ C is provable.

Hypothesis

Ref	Expression
elimel.1	⊢ B ∈ C

Assertion

Ref	Expression
elimel	⊢ if(A ∈ C, A, B) ∈ C

Proof of Theorem elimel

Step	Hyp	Ref	Expression
1		eleq1 1149	. 2 ⊢ (A = if(A ∈ C, A, B) → (A ∈ C ↔ if(A ∈ C, A, B) ∈ C))
2		eleq1 1149	. 2 ⊢ (B = if(A ∈ C, A, B) → (B ∈ C ↔ if(A ∈ C, A, B) ∈ C))
3		elimel.1	. 2 ⊢ B ∈ C
4	1, 2, 3	elimhyp 1790	1 ⊢ if(A ∈ C, A, B) ∈ C

Syntax hints:   ∈ wcel 1092  ifcif 1776

This theorem is referenced by:  limsuc 2361  orduninsuc 2365  rdgsuct 2983  rdglimt 2986  oawordeu 3157  unfilem3 3440  supsr 4025  addcant 4122  subclt 4140  subaddt 4145  subnegt 4149  negnegt 4157  subidt 4159  subid1t 4160  negcon1t 4167  subeq0t 4169  renegclt 4172  subdit 4184  mulzer1t 4188  mulneg1t 4196  mul2negt 4199  negdit 4200  mulcant 4208  mul0ort 4212  divmult 4220  divclt 4223  divcan1t 4228  divcan2t 4229  recidt 4235  divrect 4238  divdistrt 4246  divcan3t 4251  div1t 4258  redivcl 4274  redivclt 4276  gt0ne0t 4346  letrit 4347  ltadd1t 4348  leadd1t 4350  ltsubaddt 4353  lesubaddt 4355  lt2addt 4361  addge0t 4362  posdift 4365  ltnegt 4366  lenegt 4368  lesub0t 4374  mulge0t 4375  ltsqt 4376  recgt0t 4401  divgt0t 4402  divge0t 4403  ltdivt 4404  ltmuldivt 4406  ltrect 4417  lerect 4418  ltdiv23t 4419  le2sqt 4420  nnsubt 4451  2timest 4490  halfpost 4508  crut 4531  nn0mulclt 4554  sqe11t 4705  lt2sqet 4706  sqege0t 4708  nneo 4719  nn0opth2t 4726  sqrlem6 4736  sqrlem12 4742  sqrclt 4767  sqrgt0t 4768  sqrge0t 4769  sqr00t 4770  sqsqrt 4776  sqr2irrlem2 4778  sqr2irrlem5 4781  cjret 4829  cjcjt 4830  cjaddt 4831  cjmult 4832  absclt 4848  absmult 4849  absltt 4857  absidt 4862  absgt0t 4863  abssubt 4864  abs3lemt 4865  ruclem25 4909  ruclem29 4913  ruclem32 4916  ruclem33 4917  ruclem35 4919  ruclem37 4921  hvsubsub4t 5032  hvnegdit 5039  hvsubeq0t 5040  hvsubaddt 5042  hiidrclt 5053  normlem6 5068  normsub0t 5085  norm-iiit 5088  normsubt 5091  normpytht 5092  norm3lemt 5097  norm3adift 5098  hlimcaui 5141  occllem2 5181  occllem8 5187  projlem1 5193  projlem16 5208  projlem17 5209  projlem20 5212  projlem28 5220  projlem29 5221  pjthlem8 5232  pjthlem9 5233  pjthlem14 5238  pjth 5239  pjtht 5240  pjthut 5243  omlsi 5250  ococt 5253  axpjpjt 5260  pjoc1t 5270  pjoc2t 5274  shsclt 5283  shslejt 5351  shinclt 5352  shlubt 5355  chj0t 5414  chinclt 5416  chsscon3t 5417  chlejb1t 5429  chnlet 5431  chdmm1t 5438  chjasst 5446  chne0t 5452  h1de2ct 5461  spansnt 5464  elspansnt 5471  elspansn2t 5472  h1datomt 5484  pjoml3t 5517  spansnjt 5540  spansncvt 5543  pjch1t 5560  pjadjt 5576  pjaddt 5577  pjsubt 5578  pjmult 5579  pjcjt2 5580  pjcht 5582  pjss2co 5634  pjssmt 5635  pjssge0t 5636  pjdifnormt 5637  pjopytht 5662  pjnormt 5666  pjnelt 5667  chrelat2t 5761  cvexcht 5763  atcvat2t 5773

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-if 1777

metamath.org