Theorem keepel 4297

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

Syntax hints:   ∈ wcel 2137  ifcif 4228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-if 4229

This theorem is referenced by:  ifex  4298  xaddf  12246  sadcf  15375  ramcl  15933  setcepi  16937  abvtrivd  19040  mvrf1  19625  mplcoe3  19666  psrbagsn  19695  evlslem1  19715  marep01ma  20666  dscmet  22576  dscopn  22577  i1f1lem  23653  i1f1  23654  itg2const  23704  cxpval  24607  cxpcl  24617  recxpcl  24618  sqff1o  25105  chtublem  25133  dchrmulid2  25174  bposlem1  25206  lgsval  25223  lgsfcl2  25225  lgscllem  25226  lgsval2lem  25229  lgsneg  25243  lgsdilem  25246  lgsdir2  25252  lgsdir  25254  lgsdi  25256  lgsne0  25257  dchrisum0flblem1  25394  dchrisum0flblem2  25395  dchrisum0fno1  25397  rpvmasum2  25398  omlsi  28570  sgnsf  30036  psgnfzto1stlem  30157  indfval  30385  ddemeas  30606  eulerpartlemb  30737  eulerpartlemgs2  30749  sqdivzi  31915  poimirlem16  33736  poimirlem19  33739  pw2f1ocnv  38104  flcidc  38244  arearect  38301  ifcli  39826  sqwvfourb  40947  fouriersw  40949  hspval  41327