Theorem elimel 2384

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

Syntax hints:   e. wcel 955  ifcif 2351

This theorem is referenced by:  orduninsuc 3104  rdgsuct 3930  rdglimt 3933  oawordeu 4173  unfilem3 4526  supsr 5203  addcant 5324  subclt 5339  subaddt 5347  negsubt 5354  negnegt 5365  subidt 5367  subid1t 5368  neg11t 5381  renegclt 5409  mul01t 5415  mulneg1t 5423  mul2negt 5426  negdit 5427  msqgt0t 5589  msqge0t 5590  gt0ne0t 5592  ltadd1t 5597  leadd1t 5599  ltsubaddt 5601  lesubaddt 5603  lt2addt 5617  le2addt 5618  addgt0t 5620  addgegt0t 5621  addge0t 5623  ltnegt 5628  lenegt 5630  lesub0t 5651  mulge0t 5652  mulcant2 5660  mul0ort 5665  divmult 5676  divclt 5681  divcan1t 5689  divcan2t 5690  recne0t 5695  recidt 5698  divrect 5702  divdirt 5713  divcan3t 5718  div11t 5721  div1t 5729  redivcl 5754  redivclt 5756  eqnegt 5761  prodgt0t 5782  prodge0t 5784  ltmul1t 5786  ltdiv1t 5805  ltmuldivt 5817  ltrect 5832  lerect 5833  lt2msqt 5834  le2msqt 5851  nnsubt 5904  2timest 5951  halfpost 5983  nn0mulclt 6070  nneot 6145  peano5uzt 6152  icoshftf1olem 6343  icoun 6346  snunioo 6348  sq0t 6550  sq11t 6560  sqge0t 6564  sqeqort 6580  binom2t 6581  nn0opth2t 6598  sqrlem6 6608  sqrlem12 6614  sqrclt 6640  sqrgt0t 6641  sqrge0t 6642  sqrlet 6643  sqr00t 6644  sqrsqt 6652  sqsqrt 6653  sqr2irrlem2 6655  sqr2irrlem5 6658  crut 6668  reret 6734  cjrebt 6735  cjmulrclt 6736  cjmulvalt 6737  cjmulge0t 6738  renegt 6739  readdt 6740  imnegt 6742  imaddt 6743  cjcjt 6746  cjaddt 6747  cjmult 6748  cjnegt 6749  addcjt 6750  absval2t 6787  abs00t 6788  absge0t 6789  absmult 6793  absdivt 6795  absidt 6797  absltt 6817  abslttOLD 6818  abslet 6819  cjdivt 6827  absgt0t 6831  abssubt 6832  abstrit 6835  abs3lemt 6844  faclbnd4lem2 6886  bcpasct 6908  clm4at 7028  clmi2at 7029  climconst3 7033  iserzshft2 7044  serzclim0 7046  climub 7090  cvgcmp3cet 7126  expcnvlem3 7164  cvgratlem2ALT 7183  reefclt 7260  efcjt 7279  efaddlem24 7303  efaddt 7309  eftlext 7320  ef1tlub 7324  ef01tlub 7327  absef01tlub 7329  eirr 7335  ef4pt 7341  efgt0t 7346  reeff1 7350  efcnlem4 7362  reefiso 7370  sinaddt 7395  cosaddt 7396  ruclem25 7477  ruclem29 7481  ruclem32 7484  ruclem33 7485  ruclem35 7487  ruclem37 7489  methaus 7821  elimnv 8252  elimnvu 8253  nmlno0i 8386  nmblolbi 8391  blocn 8398  elimphu 8411  cosh111t 8632  efifolem1 8637  efifolem3 8639  efif1lem6 8650  hvsubsub4t 8848  hvnegdit 8855  hvsubeq0t 8856  hvaddcant 8858  hvsubaddt 8865  normlem6 8902  normlem9at 8908  normsqt 8922  normsub0t 8924  norm-iit 8926  norm-iiit 8928  normsubt 8931  normpytht 8933  norm3dift 8938  norm3lemt 8940  norm3adift 8941  normpart 8943  polidt 8947  bcst 8969  hlimcaui 9027  hhssnvt 9055  occllem2 9090  occllem8 9096  projlem1 9102  projlem16 9117  projlem17 9118  projlem20 9121  projlem28 9129  projlem29 9130  pjthlem8 9141  pjthlem9 9142  pjthlem14 9147  pjth 9148  pjtht 9149  pjtheut 9151  omlsi 9160  ococt 9163  axpjpjt 9171  pjoc1t 9182  pjomlt 9184  pjoc2t 9187  shsclt 9197  shslejt 9265  shinclt 9266  shlubt 9269  chm0t 9329  chne0t 9332  chocint 9333  chj0t 9335  chinclt 9337  chsscon3t 9338  chlejb1t 9350  chnlet 9352  chjot 9353  chdmm1t 9363  chjasst 9371  ledit 9378  h1de2ct 9395  spansnt 9398  elspansnt 9405  elspansn2t 9406  h1datomt 9422  cmbr3t 9468  pjoml2t 9471  pjoml3t 9472  cmcmt 9474  cmcm3t 9475  lecmt 9477  osumt 9505  spansnjt 9509  spansncvt 9515  pjch1t 9532  pjadjt 9547  pjaddt 9548  pjinormt 9549  pjsubt 9550  pjmult 9551  pjige0t 9553  pjcjt2 9554  pjcht 9556  pjfot 9568  pj11t 9576  pjopytht 9582  pjnormt 9586  pjpytht 9587  pjnelt 9588  eigret 9678  eigortht 9681  hoddit 9830  nmlnop0t 9838  lnopeq0lem2 9846  lnopeqt 9849  lnopunilem2 9851  lnopuni 9852  lnophm 9858  nmbdoplbt 9865  nmcopext 9874  nmcoplbt 9875  lnopcont 9879  lnfn0t 9891  lnfnmult 9892  nmcfnext 9903  nmcfnlbt 9904  lnfncont 9906  riesz4t 9912  riesz1t 9913  cnlnadjeut 9926  pjhmopt 9988  pjss2co 10003  pjssmt 10004  pjssge0t 10005  pjdifnormt 10006  pjidmcot 10019  mdslmd1lem3 10162  mdslmd1lem4 10163  csmdsym 10169  cvmdt 10171  hatomict 10195  chrelat2t 10205  cvexcht 10209  atordt 10223  atcvat2t 10224  mdsymt 10247  abs2sqlet 10279  abs2sqltt 10280  cayleythlem 10320  moec 10357  intprd 10367  ishomd 10562

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-if 2352

Copyright terms: Public domain