Theorem ifcli 4516

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

Syntax hints:   ∈ wcel 2113  ifcif 4470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1780  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-if 4471

This theorem is referenced by:  ifex  4518  xaddf  12620  sadcf  15805  ramcl  16368  setcepi  17351  abvtrivd  19614  mvrf1  20208  mplcoe3  20250  psrbagsn  20278  evlslem1  20298  marep01ma  21272  dscmet  23185  dscopn  23186  i1f1lem  24293  i1f1  24294  itg2const  24344  cxpval  25250  cxpcl  25260  recxpcl  25261  sqff1o  25762  chtublem  25790  dchrmulid2  25831  bposlem1  25863  lgsval  25880  lgsfcl2  25882  lgscllem  25883  lgsval2lem  25886  lgsneg  25900  lgsdilem  25903  lgsdir2  25909  lgsdir  25911  lgsdi  25913  lgsne0  25914  dchrisum0flblem1  26087  dchrisum0flblem2  26088  dchrisum0fno1  26090  rpvmasum2  26091  omlsi  29184  psgnfzto1stlem  30746  sgnsf  30808  indfval  31279  ddemeas  31499  eulerpartlemb  31630  eulerpartlemgs2  31642  ex-sategoelel12  32678  sqdivzi  32963  poimirlem16  34912  poimirlem19  34915  pw2f1ocnv  39640  flcidc  39780  arearect  39828  limsup10exlem  42059  sqwvfourb  42521  fouriersw  42523  hspval  42898