Theorem ifcli 4502

Description: Inference associated with ifcl 4500. Membership (closure) of a conditional operator. Also usable to keep a membership hypothesis for the weak deduction theorem dedth 4513 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 4500	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)
4	1, 2, 3	mp2an 698	1 ⊢ if(𝜑, 𝐴, 𝐵) ∈ 𝐶

Syntax hints:   ∈ wcel 2119  ifcif 4454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-if 4455

This theorem is referenced by:  ifex  4505  indfval  12157  xaddf  13167  sadcf  16413  ramcl  16991  setcepi  18046  abvtrivd  20804  mvrf1  21960  mplcoe3  22014  psrbagsn  22039  evlslem1  22058  psdmplcl  22150  psdmul  22154  psdmvr  22157  marep01ma  22643  dscmet  24555  dscopn  24556  i1f1lem  25674  i1f1  25675  itg2const  25725  cxpval  26646  cxpcl  26656  recxpcl  26657  sqff1o  27163  chtublem  27192  dchrmullid  27233  bposlem1  27265  lgsval  27282  lgsfcl2  27284  lgscllem  27285  lgsval2lem  27288  lgsneg  27302  lgsdilem  27305  lgsdir2  27311  lgsdir  27313  lgsdi  27315  lgsne0  27316  dchrisum0flblem1  27489  dchrisum0flblem2  27490  dchrisum0fno1  27492  rpvmasum2  27493  omlsi  31493  psgnfzto1stlem  33181  sgnsf  33243  ddemeas  34420  eulerpartlemb  34552  eulerpartlemgs2  34564  ex-sategoelel12  35655  sqdivzi  35956  poimirlem16  38003  poimirlem19  38006  pw2f1ocnv  43482  flcidc  43615  arearect  43660  sqrtcval  44085  sqrtcval2  44086  resqrtval  44087  imsqrtval  44088  limsup10exlem  46215  sqwvfourb  46672  fouriersw  46674  hspval  47052