Theorem ifcld 4529

Description: Membership (closure) of a conditional operator, deduction form. (Contributed by SO, 16-Jul-2018.)

Hypotheses

Ref	Expression
ifcld.a	⊢ (𝜑 → 𝐴 ∈ 𝐶)
ifcld.b	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Assertion

Ref	Expression
ifcld	⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Proof of Theorem ifcld

Step	Hyp	Ref	Expression
1		ifcld.a	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
2		ifcld.b	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
3		ifcl 4528	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
4	1, 2, 3	syl2anc 593	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2144  ifcif 4482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-if 4483

This theorem is referenced by:  ifexd  4531  soltmin  6125  pw2f1olem  9055  unxpdomlem3  9204  wemaplem2  9497  cantnfp1lem1  9635  cantnfp1lem2  9636  cantnfp1lem3  9637  cantnflem1d  9645  cantnflem1  9646  ssfzunsnext  13576  tpf  14514  relexpsucnnr  15040  rexuzre  15382  rexico  15383  limsupgre  15510  rlim3  15527  o1lo1  15566  rlimclim1  15574  lo1resb  15593  o1resb  15595  o1of2  15642  o1rlimmul  15648  lo1le  15681  ruclem1  16265  ruclem10  16273  bitsfzo  16471  ramub1lem2  17065  ramcl  17067  prmocl  17072  prmop1  17076  prmdvdsprmo  17080  prmolefac  17084  prmodvdslcmf  17085  prmgapprmo  17100  setsstruct2  17212  wunress  17287  opifismgm  18695  mulgfval  19113  frgpuptf  19812  gsumzsplit  19969  gsummpt1n0  20007  xrsds  21464  uvcvvcl2  21842  uvcff  21845  snifpsrbag  21974  psr1cl  22014  subrgpsr  22031  mvrf  22038  mplmon  22090  mplmonmul  22091  mplcoe1  22092  evlslem3  22135  evlslem1  22137  selvvvval  22197  coe1tmfv2  22340  gsummoncoe1  22373  rhmmpl  22445  rhmply1vr1  22449  mamumat1cl  22501  dmatmulcl  22562  scmatscmiddistr  22570  1mavmul  22610  marrepeval  22625  marrepcl  22626  marepveval  22630  marepvcl  22631  mdetrsca2  22666  mdetr0  22667  mdetrlin2  22669  mdetralt2  22671  mdetero  22672  mdetunilem2  22675  mdetunilem5  22678  mdetunilem6  22679  mdetunilem8  22681  mdetunilem9  22682  maducoeval2  22702  maduf  22703  madutpos  22704  madugsum  22705  gsummatr01lem3  22719  marep01ma  22722  smadiadetglem2  22734  monmatcollpw  22841  pmatcollpw3fi1lem1  22848  pmatcollpw3fi1lem2  22849  xkopt  23717  tsmssplit  24214  ssblex  24490  stdbdxmet  24577  stdbdmet  24578  stdbdbl  24579  stdbdmopn  24580  nlmvscnlem1  24748  tgioo  24858  xrsxmet  24872  icccmplem2  24886  ipcnlem1  25309  ivthlem2  25516  ovolicc2lem5  25585  ioombl1lem1  25622  ioombl1lem3  25624  ioombl1lem4  25625  mbfmax  25713  i1fres  25769  itg1climres  25778  mbfi1fseqlem3  25781  mbfi1fseqlem4  25782  mbfi1fseqlem5  25783  limcres  25950  dvferm1lem  26048  dvferm2lem  26050  dvlip2  26059  lhop1  26078  dvfsumrlim  26095  mdegaddle  26136  deg1addle2  26164  deg1sublt  26172  ply1divmo  26198  plyaddlem1  26275  plyaddlem  26277  coeaddlem  26311  dgradd2  26330  plydiveu  26364  abelthlem9  26505  logcnlem2  26710  logcnlem3  26711  cxpcn3lem  26814  lgamgulmlem4  27098  lgamgulmlem6  27100  ftalem2  27140  gausslemma2dlem4  27435  chebbnd1lem1  27535  dchrisumlem3  27557  dchrvmasumiflem1  27567  ostth3  27704  abssval  28334  absscl  28335  axlowdimlem15  29159  elrspunsn  33617  ply1moneq  33786  deg1addlt  33798  mplasclco  33815  selvply1rhmlem2  33820  extvfvv  33833  extvfvvcl  33834  extvfvcl  33835  mplvrpmrhm  33846  psrmon  33848  psrmonmul  33849  psrmonprod  33851  mplmonprod  33853  esplyfval0  33863  esplyfval1  33872  esplyind  33874  fldextrspunlsp  33973  dstfrvunirn  34774  circlemeth  34936  indispconn  35589  ex-sategoelel  35776  ex-sategoelelomsuc  35781  knoppndvlem18  36972  itg2addnclem2  38176  itg2addnclem3  38177  ftc1anclem5  38201  sticksstones10  42777  sticksstones12a  42779  aks6d1c6lem3  42794  rhmpsr  43170  evlsbagval  43173  fsuppind  43177  fsuppssind  43180  mhpind  43181  dffltz  43221  irrapxlem4  43407  irrapxlem5  43408  kelac1  43645  areaquad  43798  cantnfresb  43906  sqrtcval  44222  clsk1indlem4  44625  mnringmulrcld  44809  refsum2cnlem1  45622  rexabslelem  45997  uzublem  46009  ioondisj2  46074  ioondisj1  46075  uzubioo  46146  mullimc  46197  mullimcf  46204  lptioo2  46212  limcleqr  46223  0ellimcdiv  46228  limsupubuzlem  46291  limsupequzmptlem  46307  climxrre  46329  limsup10exlem  46351  limsup10ex  46352  liminf10ex  46353  liminflelimsuplem  46354  icccncfext  46466  cncfiooicclem1  46472  ioodvbdlimc1lem2  46511  ioodvbdlimc2lem  46513  stoweid  46642  fourierdlem9  46695  fourierdlem10  46696  fourierdlem37  46723  fourierdlem40  46726  fourierdlem66  46751  fourierdlem73  46758  fourierdlem74  46759  fourierdlem75  46760  fourierdlem78  46763  fourierdlem79  46764  fourierdlem95  46780  fourierdlem103  46788  sqwvfoura  46807  fouriersw  46810  etransclem1  46814  etransclem4  46817  etransclem17  46830  etransclem18  46831  etransclem19  46832  etransclem20  46833  etransclem21  46834  etransclem22  46835  etransclem23  46836  etransclem27  46840  etransclem32  46845  etransclem35  46848  etransclem46  46859  ioorrnopnlem  46883  ovnval2  47124  volicorecl  47125  hoiprodcl  47126  ovnf  47142  hsphoif  47155  hsphoival  47158  hoiprodcl3  47159  volicore  47160  hoidmvcl  47161  hsphoidmvle2  47164  hsphoidmvle  47165  hoidmv1lelem1  47170  hoidmv1lelem2  47171  hoidmv1lelem3  47172  hoidmvlelem2  47175  hoidmvlelem3  47176  ovnhoilem1  47180  hoidifhspf  47197  hoidifhspval3  47198  ovolval4lem1  47228  ovolval4lem2  47229  smfmullem1  47370  smfmullem2  47371  smfmullem3  47372  afv2ex  47813  suppmptcfin  49003  linc1  49052  lcoss  49063  el0ldep  49093