Theorem keepel 4105

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 2676	. 2 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
2		eleq1 2676	. 2 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
3		keepel.1	. 2 ⊢ 𝐴 ∈ 𝐶
4		keepel.2	. 2 ⊢ 𝐵 ∈ 𝐶
5	1, 2, 3, 4	keephyp 4102	1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶

Syntax hints:   ∈ wcel 1977  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  ifex  4106  xaddf  11929  sadcf  15013  ramcl  15571  setcepi  16561  abvtrivd  18663  mvrf1  19246  mplcoe3  19287  psrbagsn  19316  evlslem1  19336  marep01ma  20285  dscmet  22187  dscopn  22188  i1f1lem  23262  i1f1  23263  itg2const  23313  cxpval  24210  cxpcl  24220  recxpcl  24221  sqff1o  24708  chtublem  24736  dchrmulid2  24777  bposlem1  24809  lgsval  24826  lgsfcl2  24828  lgscllem  24829  lgsval2lem  24832  lgsneg  24846  lgsdilem  24849  lgsdir2  24855  lgsdir  24857  lgsdi  24859  lgsne0  24860  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dchrisum0fno1  25000  rpvmasum2  25001  omlsi  27647  sgnsf  29060  psgnfzto1stlem  29181  indfval  29406  ddemeas  29626  eulerpartlemb  29757  eulerpartlemgs2  29769  sqdivzi  30863  poimirlem16  32595  poimirlem19  32598  pw2f1ocnv  36622  flcidc  36763  arearect  36820  sqwvfourb  39122  fouriersw  39124  hspval  39499