Theorem keepel 4104

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

Hypotheses

Ref	Expression
keepel.1	⊢ 𝐴 ∈ 𝐶
keepel.2	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
keepel	⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶

Proof of Theorem keepel

Step	Hyp	Ref	Expression
1		eleq1 2675	. 2 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
2		eleq1 2675	. 2 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
3		keepel.1	. 2 ⊢ 𝐴 ∈ 𝐶
4		keepel.2	. 2 ⊢ 𝐵 ∈ 𝐶
5	1, 2, 3, 4	keephyp 4101	1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶

Syntax hints:   ∈ wcel 1976  ifcif 4035

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-if 4036

This theorem is referenced by:  ifex  4105  xaddf  11891  sadcf  14962  ramcl  15520  setcepi  16510  abvtrivd  18612  mvrf1  19195  mplcoe3  19236  psrbagsn  19265  evlslem1  19285  marep01ma  20233  dscmet  22135  dscopn  22136  i1f1lem  23207  i1f1  23208  itg2const  23258  cxpval  24155  cxpcl  24165  recxpcl  24166  sqff1o  24653  chtublem  24681  dchrmulid2  24722  bposlem1  24754  lgsval  24771  lgsfcl2  24773  lgscllem  24774  lgsval2lem  24777  lgsneg  24791  lgsdilem  24794  lgsdir2  24800  lgsdir  24802  lgsdi  24804  lgsne0  24805  dchrisum0flblem1  24942  dchrisum0flblem2  24943  dchrisum0fno1  24945  rpvmasum2  24946  omlsi  27481  sgnsf  28894  psgnfzto1stlem  29015  indfval  29240  ddemeas  29460  eulerpartlemb  29591  eulerpartlemgs2  29603  sqdivzi  30697  poimirlem16  32419  poimirlem19  32422  pw2f1ocnv  36446  flcidc  36587  arearect  36644  sqwvfourb  38946  fouriersw  38948  hspval  39323