Theorem elimel 2390

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 1531	. 2 ⊢ (A = if(A ∈ C, A, B) → (A ∈ C ↔ if(A ∈ C, A, B) ∈ C))
2		eleq1 1531	. 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 2386	1 ⊢ if(A ∈ C, A, B) ∈ C

Syntax hints:   ∈ wcel 956   ifcif 2357

This theorem is referenced by:  orduninsuc 3109  rdgsuct 3936  rdglimt 3939  oawordeu 4179  unfilem3 4532  supsr 5211  addcant 5332  subclt 5347  subaddt 5355  negsubt 5362  negnegt 5373  subidt 5375  subid1t 5376  neg11t 5389  renegclt 5417  mul01t 5423  mulneg1t 5431  mul2negt 5434  negdit 5435  msqgt0t 5597  msqge0t 5598  gt0ne0t 5600  ltadd1t 5605  leadd1t 5607  ltsubaddt 5609  lesubaddt 5611  lt2addt 5625  le2addt 5626  addgt0t 5628  addgegt0t 5629  addge0t 5631  ltnegt 5636  lenegt 5638  lesub0t 5659  mulge0t 5660  mulcant2 5668  mul0ort 5673  divmult 5684  divclt 5689  divcan1t 5697  divcan2t 5698  recne0t 5703  recidt 5706  divrect 5710  divdirt 5721  divcan3t 5726  div11t 5729  div1t 5737  redivcl 5762  redivclt 5764  eqnegt 5769  prodgt0t 5790  prodge0t 5792  ltmul1t 5794  ltdiv1t 5813  ltmuldivt 5825  ltrect 5840  lerect 5841  lt2msqt 5842  le2msqt 5859  nnsubt 5912  2timest 5959  halfpost 5991  nn0mulclt 6078  nneot 6153  peano5uzt 6160  icoshftf1olem 6351  icoun 6354  snunioo 6356  sq0t 6558  sq11t 6568  sqge0t 6572  sqeqort 6588  binom2t 6589  nn0opth2t 6606  sqrlem6 6616  sqrlem12 6622  sqrclt 6648  sqrgt0t 6649  sqrge0t 6650  sqrlet 6651  sqr00t 6652  sqrsqt 6660  sqsqrt 6661  sqr2irrlem2 6663  sqr2irrlem5 6666  crut 6676  reret 6742  cjrebt 6743  cjmulrclt 6744  cjmulvalt 6745  cjmulge0t 6746  renegt 6747  readdt 6748  imnegt 6750  imaddt 6751  cjcjt 6754  cjaddt 6755  cjmult 6756  cjnegt 6757  addcjt 6758  absval2t 6795  abs00t 6796  absge0t 6797  absmult 6801  absdivt 6803  absidt 6805  absltt 6825  abslttOLD 6826  abslet 6827  cjdivt 6835  absgt0t 6839  abssubt 6840  abstrit 6843  abs3lemt 6852  faclbnd4lem2 6894  bcpasct 6916  clm4at 7036  clmi2at 7037  climconst3 7041  iserzshft2 7052  serzclim0 7054  climub 7098  cvgcmp3cet 7134  expcnvlem3 7172  cvgratlem2ALT 7191  reefclt 7268  efcjt 7287  efaddlem24 7311  efaddt 7317  eftlext 7328  ef1tlub 7332  ef01tlub 7335  absef01tlub 7337  eirr 7343  ef4pt 7349  efgt0t 7354  reeff1 7358  efcnlem4 7370  reefiso 7378  sinaddt 7403  cosaddt 7404  ruclem25 7485  ruclem29 7489  ruclem32 7492  ruclem33 7493  ruclem35 7495  ruclem37 7497  methaus 7834  elimnv 8265  elimnvu 8266  nmlno0i 8399  nmblolbi 8404  blocn 8411  elimphu 8424  cosh111t 8651  efifolem1 8656  efifolem3 8658  efif1lem6 8669  hvsubsub4t 8866  hvnegdit 8873  hvsubeq0t 8874  hvaddcant 8876  hvsubaddt 8883  normlem6 8920  normlem9at 8926  normsqt 8940  normsub0t 8942  norm-iit 8944  norm-iiit 8946  normsubt 8949  normpytht 8951  norm3dift 8956  norm3lemt 8958  norm3adift 8959  normpart 8961  polidt 8965  bcst 8987  hlimcaui 9045  hhssablt 9072  hhssnvt 9074  occllem2 9113  occllem8 9119  projlem1 9125  projlem16 9140  projlem17 9141  projlem20 9144  projlem28 9152  projlem29 9153  pjthlem8 9164  pjthlem9 9165  pjthlem14 9170  pjth 9171  pjtht 9172  pjtheut 9174  omlsi 9183  ococt 9186  axpjpjt 9194  pjoc1t 9205  pjomlt 9207  pjoc2t 9210  shsclt 9220  shslejt 9288  shinclt 9289  shlubt 9292  chm0t 9352  chne0t 9355  chocint 9356  chj0t 9358  chinclt 9360  chsscon3t 9361  chlejb1t 9373  chnlet 9375  chjot 9376  chdmm1t 9386  chjasst 9394  ledit 9401  h1de2ct 9418  spansnt 9421  elspansnt 9428  elspansn2t 9429  h1datomt 9445  cmbr3t 9491  pjoml2t 9494  pjoml3t 9495  cmcmt 9497  cmcm3t 9498  lecmt 9500  osumt 9528  spansnjt 9532  spansncvt 9538  pjch1t 9555  pjadjt 9570  pjaddt 9571  pjinormt 9572  pjsubt 9573  pjmult 9574  pjige0t 9576  pjcjt2 9577  pjcht 9579  pjfot 9591  pj11t 9599  pjopytht 9605  pjnormt 9609  pjpytht 9610  pjnelt 9611  eigret 9701  eigortht 9704  hoddit 9853  nmlnop0t 9861  lnopeq0lem2 9869  lnopeqt 9872  lnopunilem2 9874  lnopuni 9875  lnophm 9881  nmbdoplbt 9888  nmcopext 9897  nmcoplbt 9898  lnopcont 9902  lnfn0t 9914  lnfnmult 9915  nmcfnext 9926  nmcfnlbt 9927  lnfncont 9929  riesz4t 9935  riesz1t 9936  cnlnadjeut 9949  pjhmopt 10015  pjss2co 10030  pjssmt 10031  pjssge0t 10032  pjdifnormt 10033  pjidmcot 10047  mdslmd1lem3 10191  mdslmd1lem4 10192  csmdsym 10198  cvmdt 10200  hatomict 10224  chrelat2t 10234  cvexcht 10238  atordt 10252  atcvat2t 10253  mdsymt 10276  abs2sqlet 10308  abs2sqltt 10309  cayleythlem 10347  moec 10393  intprd 10403  ishomd 10598

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-if 2358

Copyright terms: Public domain