Theorem keepel 4188

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

Syntax hints:   ∈ wcel 2030  ifcif 4119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120

This theorem is referenced by:  ifex  4189  xaddf  12093  sadcf  15222  ramcl  15780  setcepi  16785  abvtrivd  18888  mvrf1  19473  mplcoe3  19514  psrbagsn  19543  evlslem1  19563  marep01ma  20514  dscmet  22424  dscopn  22425  i1f1lem  23501  i1f1  23502  itg2const  23552  cxpval  24455  cxpcl  24465  recxpcl  24466  sqff1o  24953  chtublem  24981  dchrmulid2  25022  bposlem1  25054  lgsval  25071  lgsfcl2  25073  lgscllem  25074  lgsval2lem  25077  lgsneg  25091  lgsdilem  25094  lgsdir2  25100  lgsdir  25102  lgsdi  25104  lgsne0  25105  dchrisum0flblem1  25242  dchrisum0flblem2  25243  dchrisum0fno1  25245  rpvmasum2  25246  omlsi  28391  sgnsf  29857  psgnfzto1stlem  29978  indfval  30206  ddemeas  30427  eulerpartlemb  30558  eulerpartlemgs2  30570  sqdivzi  31736  poimirlem16  33555  poimirlem19  33558  pw2f1ocnv  37921  flcidc  38061  arearect  38118  ifcli  39643  sqwvfourb  40764  fouriersw  40766  hspval  41144