Theorem elimel 2439

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

Hypothesis

Ref	Expression
elimel.1	|- B e. C

Assertion

Ref	Expression
elimel	|- if(A e. C, A, B) e. C

Proof of Theorem elimel

Step	Hyp	Ref	Expression
1		eleq1 1571	. 2 |- (A = if(A e. C, A, B) -> (A e. C <-> if(A e. C, A, B) e. C))
2		eleq1 1571	. 2 |- (B = if(A e. C, A, B) -> (B e. C <-> if(A e. C, A, B) e. C))
3		elimel.1	. 2 |- B e. C
4	1, 2, 3	elimhyp 2435	1 |- if(A e. C, A, B) e. C

Syntax hints:   e. wcel 990  ifcif 2406

This theorem is referenced by:  orduninsuc 3169  rdgsuc 4021  rdglim 4024  oawordeu 4273  unfilem3 4637  supsr 5320  addcan 5441  subcl 5456  subadd 5464  negsub 5471  negneg 5482  subid 5484  subid1 5485  neg11 5498  renegcl 5526  mul01 5532  mulneg1 5540  mul2neg 5543  negdi 5544  msqgt0 5704  msqge0 5705  gt0ne0 5707  ltadd1 5712  leadd1 5714  ltsubadd 5716  lesubadd 5718  lt2add 5732  le2add 5733  addgt0 5736  addgegt0 5737  addge0 5739  ltneg 5744  leneg 5746  lesub0 5767  mulge0 5768  mulcant2i 5776  mul0or 5782  divmul 5793  divmulOLD 5794  divcl 5801  divcan1 5809  recne0 5815  recid 5818  divrec 5822  divdir 5835  divdirOLD 5836  divcan3 5841  div11 5844  div1 5852  redivcli 5882  redivcl 5884  eqneg 5889  prodgt0 5910  prodge0 5912  ltmul1 5914  ltmul1OLD 5915  ltdiv1 5934  ltdiv1OLD 5935  ltmuldiv 5948  ltmuldivOLD 5949  ltrec 5971  lerec 5972  lt2msq 5973  le2msq 5990  nnsub 6045  2times 6092  halfpos 6124  nn0mulcl 6233  nneo 6311  peano5uzti 6317  icoshftf1olem 6470  icoun 6473  snunioo 6475  sq11 6751  sqge0 6755  sqeqor 6771  binom2 6772  nn0opth2 6791  sqrlem6 6801  sqrlem12 6807  sqrcl 6833  sqrgt0 6834  sqrge0 6835  sqrle 6836  sqr00 6837  sqrsq 6845  sqsqr 6846  sqr2irrlem2 6848  sqr2irrlem5 6851  cru 6861  cjreb 6923  cjmulrcl 6924  cjmulval 6925  cjmulge0 6926  reneg 6927  readd 6928  imneg 6930  imadd 6931  cjcj 6934  cjadd 6935  cjmul 6936  cjneg 6937  addcj 6938  absval2 6975  abs00 6976  absge0 6977  absmul 6981  absdiv 6983  absid 6985  abslt 7003  absle 7004  cjdiv 7012  absgt0 7016  abssub 7017  abstri 7021  abs3lem 7030  faclbnd4lem2 7072  bcpasc 7093  clm4a 7213  clmi2a 7214  climconst3 7219  iserzshft2i 7230  serzclim0 7232  climubi 7277  cvgcmp3ce 7313  expcnvlem3 7352  cvgratlem2ALT 7371  reefcl 7441  efcj 7460  efaddlem24 7484  efadd 7490  eftlex 7501  ef1tlubi 7505  ef01tlubi 7509  absef01tlubi 7511  eirr 7517  ef4p 7524  efgt0 7529  reef11 7533  efcnlem4 7546  reefiso 7552  sinadd 7577  cosadd 7578  ruclem25 7659  ruclem29 7663  ruclem32 7666  ruclem33 7667  ruclem35 7669  ruclem37 7671  methaus 8002  elimnv 8433  elimnvu 8434  nmlno0i 8573  nmblolbi 8579  blocn 8586  elimphu 8599  cosh111 8836  efifolem1 8841  efifolem3 8843  efif1lem6 8854  hvsubsub4 9046  hvnegdi 9053  hvsubeq0 9054  hvaddcan 9056  hvsubadd 9064  normlem6 9101  normlem9at 9107  normsq 9121  normsub0 9123  norm-ii 9125  norm-iii 9127  normsub 9130  normpyth 9132  norm3dif 9137  norm3lemt 9139  norm3adifi 9140  normpar 9142  polid 9146  bcs 9168  hlimcauii 9226  hhssabl 9253  hhssnvt 9255  occllem2 9294  occllem8 9300  projlem1 9306  projlem16 9321  projlem17 9322  projlem20 9325  projlem28 9333  projlem29 9334  pjthlem8 9346  pjthlem9 9347  pjthlem14 9352  pjthi 9353  pjth 9354  pjtheu 9356  omlsii 9365  ococ 9368  axpjpj 9376  pjoc1 9387  pjoml 9389  pjoc2 9392  shscl 9402  shslej 9470  shincl 9471  shlub 9474  chm0 9534  chne0 9537  chocin 9538  chj0 9540  chincl 9542  chsscon3 9543  chlejb1 9555  chnle 9557  chjo 9558  chdmm1 9568  chjass 9576  ledi 9583  h1de2ci 9599  spansn 9602  elspansn 9609  elspansn2 9610  h1datom 9625  cmbr3 9671  pjoml2 9674  pjoml3 9675  cmcm 9677  cmcm3 9678  lecm 9680  osum 9708  spansnj 9712  spansncv 9718  pjch1 9735  pjadji 9750  pjaddi 9751  pjinormi 9752  pjsubi 9753  pjmuli 9754  pjige0 9756  pjcjt2 9757  pjch 9759  pjfo 9771  pj11 9779  pjopyth 9785  pjnorm 9789  pjpyth 9790  pjnel 9791  eigre 9881  hmopbdoptHIL 10030  hoddi 10032  nmlnop0 10040  lnopeq0lem2 10048  lnopeq 10051  lnopunilem2 10053  lnopunii 10054  lnophmi 10060  nmbdoplb 10067  nmcopex 10076  nmcoplb 10077  lnopcon 10081  lnfn0 10093  lnfnmul 10094  nmcfnex 10105  nmcfnlb 10106  lnfncon 10108  riesz4 10114  riesz1 10115  cnlnadjeu 10128  pjhmop 10194  pjss2coi 10209  pjssmi 10210  pjssge0i 10211  pjdifnormi 10212  pjidmco 10226  mdslmd1lem3 10372  mdslmd1lem4 10373  csmdsymi 10379  cvmd 10381  hatomic 10405  chrelat2 10415  cvexch 10419  atord 10433  atcvat2 10434  mdsym 10457  abs2sqlet 10495  abs2sqltt 10496  cayleythlem 10534  moec 10579  intprd 10589  subspemp2 10693  limfillem2OLD 10732  ishomd 10853

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-12 1000  ax-17 1003  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251  ax-ext 1494

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1013  df-sb 1205  df-clab 1500  df-cleq 1505  df-clel 1508  df-if 2407

Copyright terms: Public domain