Theorem elimel 4150

Description: Eliminate a membership hypothesis for weak deduction theorem, when special case 𝐵 ∈ 𝐶 is provable. (Contributed by NM, 15-May-1999.)

Hypothesis

Ref	Expression
elimel.1	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
elimel	⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶

Proof of Theorem elimel

Step	Hyp	Ref	Expression
1		eleq1 2689	. 2 ⊢ (𝐴 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶))
2		eleq1 2689	. 2 ⊢ (𝐵 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶))
3		elimel.1	. 2 ⊢ 𝐵 ∈ 𝐶
4	1, 2, 3	elimhyp 4146	1 ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶

Syntax hints:   ∈ wcel 1990  ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  fprg  6422  orduninsuc  7043  oawordeu  7635  oeoa  7677  omopth  7738  unfilem3  8226  inar1  9597  supsr  9933  renegcl  10344  peano5uzti  11467  eluzadd  11716  eluzsub  11717  ltweuz  12760  uzenom  12763  seqfn  12813  seq1  12814  seqp1  12816  sqeqor  12978  binom2  12979  nn0opth2  13059  faclbnd4lem2  13081  hashxp  13221  dvdsle  15032  divalglem7  15122  divalg  15126  gcdaddm  15246  smadiadetr  20481  iblcnlem  23555  ax5seglem8  25816  elimnv  27538  elimnvu  27539  nmlno0i  27649  nmblolbi  27655  blocn  27662  elimphu  27676  ubth  27729  htth  27775  ifhvhv0  27879  normlem6  27972  norm-iii  27997  norm3lemt  28009  ifchhv  28101  hhssablo  28120  hhssnvt  28122  shscl  28177  shslej  28239  shincl  28240  omlsii  28262  pjoml  28295  pjoc2  28298  chm0  28350  chne0  28353  chocin  28354  chj0  28356  chlejb1  28371  chnle  28373  ledi  28399  h1datom  28441  cmbr3  28467  pjoml2  28470  cmcm  28473  cmcm3  28474  lecm  28476  pjmuli  28548  pjige0  28550  pjhfo  28565  pj11  28573  eigre  28694  eigorth  28697  hoddi  28849  nmlnop0  28857  lnopeq  28868  lnopunilem2  28870  nmbdoplb  28884  nmcopex  28888  nmcoplb  28889  lnopcon  28894  lnfn0  28906  lnfnmul  28907  nmcfnex  28912  nmcfnlb  28913  lnfncon  28915  riesz4  28923  riesz1  28924  cnlnadjeu  28937  pjhmop  29009  pjidmco  29040  mdslmd1lem3  29186  mdslmd1lem4  29187  csmdsymi  29193  hatomic  29219  atord  29247  atcvat2  29248  bnj941  30843  bnj944  31008  kur14  31198  abs2sqle  31574  abs2sqlt  31575  onsucconn  32437  onsucsuccmp  32443  sdclem1  33539  bnd2d  42428