Theorem elimel 4551

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 2848	. 2 ⊢ (𝐴 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶))
2		eleq1 2848	. 2 ⊢ (𝐵 = if(𝐴 ∈ 𝐶, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶))
3		elimel.1	. 2 ⊢ 𝐵 ∈ 𝐶
4	1, 2, 3	elimhyp 4547	1 ⊢ if(𝐴 ∈ 𝐶, 𝐴, 𝐵) ∈ 𝐶

This proof depends on syntax axioms:   ∈ wcel 2144  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  fprg  7159  orduninsuc  7854  oawordeu  8566  oeoa  8609  omopth  8674  unfilem3  9302  bnd2d  9971  inar1  10863  supsr  11200  renegcl  11624  peano5uzti  12792  ltweuz  14107  uzenom  14110  seqfn  14159  seq1  14160  seqp1  14162  sqeqor  14363  binom2  14364  nn0opth2  14419  faclbnd4lem2  14441  hashxp  14582  dvdsle  16485  divalglem7  16574  divalg  16578  gcdaddm  16702  smadiadetr  22995  iblcnlem  26114  ax5seglem8  29519  elimnv  31290  elimnvu  31291  nmlno0i  31401  nmblolbi  31407  blocn  31414  elimphu  31428  ubth  31480  htth  31525  ifhvhv0  31629  normlem6  31722  norm-iii  31747  norm3lemt  31759  ifchhv  31851  hhssablo  31870  hhssnvt  31872  shscl  31925  shslej  31987  shincl  31988  omlsii  32010  pjoml  32043  pjoc2  32046  chm0  32098  chne0  32101  chocin  32102  chj0  32104  chlejb1  32119  chnle  32121  ledi  32147  h1datom  32189  cmbr3  32215  pjoml2  32218  cmcm  32221  cmcm3  32222  lecm  32224  pjmuli  32296  pjige0  32298  pjhfo  32313  pj11  32321  eigre  32442  eigorth  32445  hoddi  32597  nmlnop0  32605  lnopeq  32616  lnopunilem2  32618  nmbdoplb  32632  nmcopex  32636  nmcoplb  32637  lnopcon  32642  lnfn0  32654  lnfnmul  32655  nmcfnex  32660  nmcfnlb  32661  lnfncon  32663  riesz4  32671  riesz1  32672  cnlnadjeu  32685  pjhmop  32757  pjidmco  32788  mdslmd1lem3  32934  mdslmd1lem4  32935  csmdsymi  32941  hatomic  32967  atord  32995  atcvat2  32996  bnj941  35449  bnj944  35614  kur14  36067  abs2sqle  36531  abs2sqlt  36532  onsucconn  37318  onsucsuccmp  37324  sdclem1  38770  mnurnd  45360