Theorem ifcli 4595

Description: Inference associated with ifcl 4593. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4606 when the special case 𝐵 ∈ 𝐶 is provable. (Contributed by NM, 14-Aug-1999.) (Proof shortened by BJ, 1-Sep-2022.)

Hypotheses

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

Assertion

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

Proof of Theorem ifcli

Step	Hyp	Ref	Expression
1		ifcli.1	. 2 ⊢ 𝐴 ∈ 𝐶
2		ifcli.2	. 2 ⊢ 𝐵 ∈ 𝐶
3		ifcl 4593	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)
4	1, 2, 3	mp2an 691	1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶

Syntax hints:   ∈ wcel 2103  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2712  df-cleq 2726  df-clel 2813  df-if 4549

This theorem is referenced by:  ifex  4598  xaddf  13282  sadcf  16493  ramcl  17071  setcepi  18150  abvtrivd  20850  mvrf1  22023  mplcoe3  22073  psrbagsn  22104  evlslem1  22123  psdmplcl  22182  psdmul  22186  marep01ma  22680  dscmet  24599  dscopn  24600  i1f1lem  25736  i1f1  25737  itg2const  25788  cxpval  26715  cxpcl  26725  recxpcl  26726  sqff1o  27234  chtublem  27264  dchrmullid  27305  bposlem1  27337  lgsval  27354  lgsfcl2  27356  lgscllem  27357  lgsval2lem  27360  lgsneg  27374  lgsdilem  27377  lgsdir2  27383  lgsdir  27385  lgsdi  27387  lgsne0  27388  dchrisum0flblem1  27561  dchrisum0flblem2  27562  dchrisum0fno1  27564  rpvmasum2  27565  omlsi  31427  psgnfzto1stlem  33085  sgnsf  33147  indfval  33972  ddemeas  34192  eulerpartlemb  34325  eulerpartlemgs2  34337  ex-sategoelel12  35387  sqdivzi  35682  poimirlem16  37544  poimirlem19  37547  pw2f1ocnv  42931  flcidc  43071  arearect  43116  sqrtcval  43543  sqrtcval2  43544  resqrtval  43545  imsqrtval  43546  limsup10exlem  45627  sqwvfourb  46084  fouriersw  46086  hspval  46464