Theorem elimel 3025

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

Syntax hints:   e. wcel 1300  ifcif 2982

This theorem is referenced by:  orduninsuc 3925  rdgsuc 5153  rdglim 5156  oawordeu 5237  oeoa 5272  unfilem3 5643  supsr 6383  addcan 6507  subcl 6524  subadd 6532  negsub 6540  negneg 6553  subid 6555  subid1 6556  neg11 6569  renegcl 6600  mul01 6606  mulneg1 6615  mul2negOLD 6619  negdi 6620  msqgt0 6797  msqge0 6798  gt0ne0 6800  ltadd1 6806  leadd1 6808  ltsubadd 6810  lesubadd 6812  lt2add 6827  le2add 6828  addgt0OLD 6832  addgegt0OLD 6834  addge0OLD 6838  ltneg 6844  leneg 6846  lesub0 6867  mulge0 6868  mulge0OLD 6869  mulcant2i 6879  mul0or 6884  divmul 6896  divcl 6901  divcan1 6909  recne0 6915  recid 6918  divrec 6922  divdir 6933  divcan3 6938  div11 6941  div1 6949  redivcli 6976  redivcl 6978  eqneg 6983  prodgt0 7004  prodge0 7006  ltmul1 7008  ltdiv1 7031  ltdiv1OLD 7032  ltmuldiv 7045  ltmuldivOLD 7046  ltrec 7067  lerec 7068  lt2msq 7069  le2msq 7086  nnsub 7141  2times 7188  halfpos 7222  nn0mulcl 7332  nneo 7410  peano5uzti 7416  icoshftf1olem 7579  icoun 7582  snunioo 7584  sq11 7874  sqge0 7878  sqeqor 7895  binom2 7896  nn0opth2 7918  sqrlem6 7928  sqrlem12 7934  sqrcl 7960  sqrgt0 7961  sqrge0 7962  sqrle 7963  sqr00 7964  sqrsq 7972  sqsqr 7973  sqr2irrlem2 7975  sqr2irrlem5 7978  cru 7988  cjreb 8050  cjmulrcl 8051  cjmulval 8052  cjmulge0 8053  reneg 8054  readd 8055  imneg 8057  imadd 8058  cjcj 8061  cjadd 8062  cjmul 8063  cjneg 8064  addcj 8065  absval2 8103  abs00 8104  absge0 8105  absmul 8109  absdiv 8111  absid 8113  abslt 8132  absle 8133  cjdiv 8141  absgt0 8145  abssub 8146  abstri 8150  abs3lem 8159  faclbnd4lem2 8201  bcpasc 8222  clm4a 8350  clmi2a 8351  climconst3 8356  iserzshft2i 8367  serzclim0 8369  climubi 8414  cvgcmp3ce 8451  expcnvlem3 8490  cvgratlem2ALT 8510  reefcl 8580  efcj 8599  efaddlem24 8623  efadd 8629  eftlex 8640  ef1tlubi 8644  ef01tlubi 8648  absef01tlubi 8650  eirr 8656  ef4p 8665  efgt0 8670  reef11 8674  efcnlem4 8687  reefiso 8693  sinadd 8718  cosadd 8719  ruclem25 8803  ruclem29 8807  ruclem32 8810  ruclem33 8811  ruclem35 8813  ruclem37 8815  methaus 9160  grpidval 9342  addinv 9436  elimnv 9646  elimnvu 9647  vacnlem4 9670  nmlno0i 9794  nmblolbi 9800  blocn 9807  elimphu 9821  cosh111 10071  efifolem1 10076  efifolem3 10078  efif1lem6 10089  dif1card 10177  ac6sg 10188  issubsplem1 10246  issubspt 10247  fora2 10407  hvsubsub4 10559  hvnegdi 10566  hvsubeq0 10567  hvaddcan 10569  hvsubadd 10577  normlem6 10614  normlem9at 10620  normsq 10634  normsub0 10636  norm-ii 10638  norm-iii 10640  normsub 10643  normpyth 10645  norm3dif 10650  norm3lemt 10652  norm3adifi 10653  normpar 10655  polid 10659  bcs 10681  hlimcauii 10739  hhssabl 10766  hhssnvt 10768  occllem2 10807  occllem8 10813  projlem1 10819  projlem16 10834  projlem17 10835  projlem20 10838  projlem28 10846  projlem29 10847  pjthlem8 10859  pjthlem9 10860  pjthlem14 10865  pjthi 10866  pjth 10867  pjtheu 10869  omlsii 10878  ococ 10881  axpjpj 10889  pjoc1 10900  pjoml 10902  pjoc2 10905  shscl 10915  shslej 10983  shincl 10984  shlub 10987  chm0 11047  chne0 11050  chocin 11051  chj0 11053  chincl 11055  chsscon3 11056  chlejb1 11068  chnle 11070  chjo 11071  chdmm1 11081  chjass 11089  ledi 11096  h1de2ci 11112  spansn 11115  elspansn 11122  elspansn2 11123  h1datom 11138  cmbr3 11184  pjoml2 11187  pjoml3 11188  cmcm 11190  cmcm3 11191  lecm 11193  osum 11223  spansnj 11227  spansncv 11233  pjch1 11250  pjadji 11265  pjaddi 11266  pjinormi 11267  pjsubi 11268  pjmuli 11269  pjige0 11271  pjcjt2 11272  pjch 11274  pjfo 11286  pj11 11294  pjopyth 11300  pjnorm 11304  pjpyth 11305  pjnel 11306  eigre 11398  eigorth 11401  hmopbdoptHIL 11550  hoddi 11552  nmlnop0 11560  lnopeq0lem2 11568  lnopeq 11571  lnopunilem2 11573  lnopunii 11574  lnophmi 11580  nmbdoplb 11587  nmcopex 11596  nmcoplb 11597  lnopcon 11601  lnfn0 11613  lnfnmul 11614  nmcfnex 11625  nmcfnlb 11626  lnfncon 11628  riesz4 11634  riesz1 11635  cnlnadjeu 11648  pjhmop 11721  pjss2coi 11736  pjssmi 11737  pjssge0i 11738  pjdifnormi 11739  pjidmco 11753  mdslmd1lem3 11899  mdslmd1lem4 11900  csmdsymi 11906  cvmd 11908  hatomic 11932  chrelat2 11942  cvexch 11946  atord 11960  atcvat2 11961  mdsym 11984  bnj147 12480  bnj148 12481  bnj209OLD 12501  bnj210OLD 12503  bnj211OLD 12505  bnj519 12520  bnj941 12842  bnj517 13259  bnj939 13338  fndmeng 13598  fz1eqb 13609  abs2sqle 13624  abs2sqlt 13625  cayleythlem 13645  dvdsle 13693  divalglem7 13702  divalg 13706  gcdaddm 13735  mulgcdlem6 13761  moec 14351  ac5g 14388  snelpwg 14415  pw2eng 14419  infxpg 14422  infsdomnng 14423  prnzg 14454  fprod1s1 14679  fprodp1s1 14683  fprod1i2 14685  distopg 14876  subsp2 14902  subspemp2 14904  limfillem2 14939  clindistop2 14963  topgrpsubcn 14982  ishomd 15139  erthdmg 15730  add20 15777  eluzadd 15782  eluzsub 15783  iserzshft2 15829  isumshft2 15830  txcnoprab 15911  reparpht 16065

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-if 2983

Copyright terms: Public domain