Theorem elimel 2365

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 1510	. 2 |- (A = if(A e. C, A, B) -> (A e. C <-> if(A e. C, A, B) e. C))
2		eleq1 1510	. 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 2361	1 |- if(A e. C, A, B) e. C

Syntax hints:   e. wcel 1105  ifcif 2332

This theorem is referenced by:  orduninsuc 3077  rdgsuct 3884  rdglimt 3887  oawordeu 4127  unfilem3 4478  supsr 5154  addcant 5275  subclt 5290  subaddt 5298  negsubt 5305  negnegt 5316  subidt 5318  subid1t 5319  neg11t 5332  renegclt 5360  mul01t 5366  mulneg1t 5374  mul2negt 5377  negdit 5378  msqgt0t 5540  msqge0t 5541  gt0ne0t 5543  ltadd1t 5548  leadd1t 5550  ltsubaddt 5552  lesubaddt 5554  lt2addt 5568  le2addt 5569  addgt0t 5571  addgegt0t 5572  addge0t 5574  ltnegt 5579  lenegt 5581  lesub0t 5602  mulge0t 5603  mulcant2 5611  mul0ort 5616  divmult 5627  divclt 5632  divcan1t 5640  divcan2t 5641  recne0t 5646  recidt 5649  divrect 5653  divdirt 5664  divcan3t 5669  div11t 5672  div1t 5680  redivcl 5705  redivclt 5707  eqnegt 5712  prodgt0t 5733  prodge0t 5735  ltmul1t 5737  ltdiv1t 5756  ltmuldivt 5768  ltrect 5783  lerect 5784  lt2msqt 5785  le2msqt 5802  nnsubt 5855  2timest 5902  halfpost 5934  nn0mulclt 6021  nneot 6096  peano5uzt 6103  icoshftf1olem 6294  icoun 6297  snunioo 6299  sq0t 6501  sq11t 6511  sqge0t 6515  sqeqort 6531  binom2t 6532  nn0opth2t 6549  sqrlem6 6559  sqrlem12 6565  sqrclt 6591  sqrgt0t 6592  sqrge0t 6593  sqrlet 6594  sqr00t 6595  sqrsqt 6603  sqsqrt 6604  sqr2irrlem2 6606  sqr2irrlem5 6609  crut 6619  reret 6685  cjrebt 6686  cjmulrclt 6687  cjmulvalt 6688  cjmulge0t 6689  renegt 6690  readdt 6691  imnegt 6693  imaddt 6694  cjcjt 6697  cjaddt 6698  cjmult 6699  cjnegt 6700  addcjt 6701  absval2t 6738  abs00t 6739  absge0t 6740  absmult 6744  absdivt 6746  absidt 6748  absltt 6768  abslttOLD 6769  abslet 6770  cjdivt 6778  absgt0t 6782  abssubt 6783  abstrit 6786  abs3lemt 6795  faclbnd4lem2 6837  bcpasct 6859  clm4at 6979  clmi2at 6980  climconst3 6984  iserzshft2 6995  serzclim0 6997  climub 7041  cvgcmp3cet 7077  expcnvlem3 7115  cvgratlem2ALT 7134  reefclt 7211  efcjt 7230  efaddlem24 7254  efaddt 7260  eftlext 7271  ef1tlub 7275  ef01tlub 7278  absef01tlub 7280  eirr 7286  ef4pt 7292  efgt0t 7297  reeff1 7301  efcnlem4 7313  reefiso 7321  sinaddt 7346  cosaddt 7347  ruclem25 7428  ruclem29 7432  ruclem32 7435  ruclem33 7436  ruclem35 7438  ruclem37 7440  methaus 7769  elimnv 8189  elimnvu 8190  nmlno0i 8321  nmblolbi 8326  blocn 8333  elimphu 8346  cosh111t 8545  efifolem1 8550  efifolem3 8552  efif1lem6 8563  abs2sqlet 8641  abs2sqltt 8642  symggrp 8675  cayleythlem 8680  moec 8716  intprd 8726  ishomd 8912  hvsubsub4t 9076  hvnegdit 9083  hvsubeq0t 9084  hvaddcant 9086  hvsubaddt 9093  normlem6 9130  normlem9at 9136  normsqt 9150  normsub0t 9152  norm-iit 9154  norm-iiit 9156  normsubt 9159  normpytht 9161  norm3dift 9166  norm3lemt 9168  norm3adift 9169  normpart 9171  polidt 9175  bcst 9197  hlimcaui 9257  occllem2 9304  occllem8 9310  projlem1 9316  projlem16 9331  projlem17 9332  projlem20 9335  projlem28 9343  projlem29 9344  pjthlem8 9355  pjthlem9 9356  pjthlem14 9361  pjth 9362  pjtht 9363  pjtheut 9365  omlsi 9374  ococt 9377  axpjpjt 9385  pjoc1t 9396  pjomlt 9398  pjoc2t 9401  shsclt 9411  shslejt 9479  shinclt 9480  shlubt 9483  chm0t 9543  chne0t 9546  chocint 9547  chj0t 9549  chinclt 9551  chsscon3t 9552  chlejb1t 9564  chnlet 9566  chjot 9567  chdmm1t 9577  chjasst 9585  ledit 9592  h1de2ct 9609  spansnt 9612  elspansnt 9619  elspansn2t 9620  h1datomt 9636  cmbr3t 9682  pjoml2t 9685  pjoml3t 9686  cmcmt 9688  cmcm3t 9689  lecmt 9691  osumt 9719  spansnjt 9723  spansncvt 9729  pjch1t 9746  pjadjt 9761  pjaddt 9762  pjinormt 9763  pjsubt 9764  pjmult 9765  pjige0t 9767  pjcjt2 9768  pjcht 9770  pjfot 9782  pj11t 9790  pjopytht 9796  pjnormt 9800  pjpytht 9801  pjnelt 9802  eigret 9892  eigortht 9895  hoddit 10044  nmlnop0t 10052  lnopeq0lem2 10060  lnopeqt 10063  lnopunilem2 10065  lnopuni 10066  lnophm 10072  nmbdoplbt 10079  nmcopext 10088  nmcoplbt 10089  lnopcont 10093  lnfn0t 10105  lnfnmult 10106  nmcfnext 10117  nmcfnlbt 10118  lnfncont 10120  riesz4t 10126  riesz1t 10127  cnlnadjeut 10140  pjhmopt 10202  pjss2co 10217  pjssmt 10218  pjssge0t 10219  pjdifnormt 10220  pjidmcot 10233  mdslmd1lem3 10376  mdslmd1lem4 10377  csmdsym 10383  cvmdt 10385  hatomict 10409  chrelat2t 10419  cvexcht 10423  atordt 10437  atcvat2t 10438  mdsymt 10461

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-if 2333

Copyright terms: Public domain