Theorem ifcld 4470

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 4469	. 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
4	1, 2, 3	syl2anc 587	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∈ wcel 2111  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4426

This theorem is referenced by:  soltmin  5963  pw2f1olem  8604  unxpdomlem3  8708  wemaplem2  8995  cantnfp1lem1  9125  cantnfp1lem2  9126  cantnfp1lem3  9127  cantnflem1d  9135  cantnflem1  9136  ssfzunsnext  12947  relexpsucnnr  14376  rexuzre  14704  rexico  14705  limsupgre  14830  rlim3  14847  o1lo1  14886  rlimclim1  14894  lo1resb  14913  o1resb  14915  o1of2  14961  o1rlimmul  14967  lo1le  15000  ruclem1  15576  ruclem10  15584  bitsfzo  15774  ramub1lem2  16353  ramcl  16355  prmocl  16360  prmop1  16364  prmdvdsprmo  16368  prmolefac  16372  prmodvdslcmf  16373  prmgapprmo  16388  setsstruct2  16513  wunress  16556  opifismgm  17861  mulgfval  18218  frgpuptf  18888  gsumzsplit  19040  gsummpt1n0  19078  xrsds  20134  uvcvvcl2  20477  uvcff  20480  snifpsrbag  20604  psr1cl  20640  subrgpsr  20657  mvrf  20662  mplmon  20703  mplmonmul  20704  mplcoe1  20705  evlslem3  20752  evlslem1  20754  coe1tmfv2  20904  gsummoncoe1  20933  mamumat1cl  21044  dmatmulcl  21105  scmatscmiddistr  21113  1mavmul  21153  marrepeval  21168  marrepcl  21169  marepveval  21173  marepvcl  21174  mdetrsca2  21209  mdetr0  21210  mdetrlin2  21212  mdetralt2  21214  mdetero  21215  mdetunilem2  21218  mdetunilem5  21221  mdetunilem6  21222  mdetunilem8  21224  mdetunilem9  21225  maducoeval2  21245  maduf  21246  madutpos  21247  madugsum  21248  gsummatr01lem3  21262  marep01ma  21265  smadiadetglem2  21277  monmatcollpw  21384  pmatcollpw3fi1lem1  21391  pmatcollpw3fi1lem2  21392  xkopt  22260  tsmssplit  22757  ssblex  23035  stdbdxmet  23122  stdbdmet  23123  stdbdbl  23124  stdbdmopn  23125  nlmvscnlem1  23292  tgioo  23401  xrsxmet  23414  icccmplem2  23428  ipcnlem1  23849  ivthlem2  24056  ovolicc2lem5  24125  ioombl1lem1  24162  ioombl1lem3  24164  ioombl1lem4  24165  mbfmax  24253  i1fres  24309  itg1climres  24318  mbfi1fseqlem3  24321  mbfi1fseqlem4  24322  mbfi1fseqlem5  24323  limcres  24489  dvferm1lem  24587  dvferm2lem  24589  dvlip2  24598  lhop1  24617  dvfsumrlim  24634  mdegaddle  24675  deg1addle2  24703  deg1sublt  24711  ply1divmo  24736  plyaddlem1  24810  plyaddlem  24812  coeaddlem  24846  dgradd2  24865  plydiveu  24894  abelthlem9  25035  logcnlem2  25234  logcnlem3  25235  cxpcn3lem  25336  lgamgulmlem4  25617  lgamgulmlem6  25619  ftalem2  25659  gausslemma2dlem4  25953  chebbnd1lem1  26053  dchrisumlem3  26075  dchrvmasumiflem1  26085  ostth3  26222  axlowdimlem15  26750  dstfrvunirn  31842  circlemeth  32021  indispconn  32594  ex-sategoelel  32781  ex-sategoelelomsuc  32786  noprefixmo  33315  knoppndvlem18  33981  itg2addnclem2  35109  itg2addnclem3  35110  ftc1anclem5  35134  metakunt3  39352  metakunt4  39353  metakunt29  39378  metakunt30  39379  metakunt32  39381  metakunt33  39382  fsuppind  39456  fsuppssind  39459  dffltz  39615  irrapxlem4  39766  irrapxlem5  39767  kelac1  40007  areaquad  40166  sqrtcval  40341  clsk1indlem4  40747  mnringmulrcld  40936  refsum2cnlem1  41666  rexabslelem  42055  uzublem  42067  ioondisj2  42130  ioondisj1  42131  uzubioo  42204  mullimc  42258  mullimcf  42265  lptioo2  42273  limcleqr  42286  0ellimcdiv  42291  limsupubuzlem  42354  limsupequzmptlem  42370  climxrre  42392  limsup10exlem  42414  limsup10ex  42415  liminf10ex  42416  liminflelimsuplem  42417  icccncfext  42529  cncfiooicclem1  42535  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  stoweid  42705  fourierdlem9  42758  fourierdlem10  42759  fourierdlem37  42786  fourierdlem40  42789  fourierdlem66  42814  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem78  42826  fourierdlem79  42827  fourierdlem95  42843  fourierdlem103  42851  sqwvfoura  42870  fouriersw  42873  etransclem1  42877  etransclem4  42880  etransclem17  42893  etransclem18  42894  etransclem19  42895  etransclem20  42896  etransclem21  42897  etransclem22  42898  etransclem23  42899  etransclem27  42903  etransclem32  42908  etransclem35  42911  etransclem46  42922  ioorrnopnlem  42946  ovnval2  43184  volicorecl  43185  hoiprodcl  43186  ovnf  43202  hsphoif  43215  hsphoival  43218  hoiprodcl3  43219  volicore  43220  hoidmvcl  43221  hsphoidmvle2  43224  hsphoidmvle  43225  hoidmv1lelem1  43230  hoidmv1lelem2  43231  hoidmv1lelem3  43232  hoidmvlelem2  43235  hoidmvlelem3  43236  ovnhoilem1  43240  hoidifhspf  43257  hoidifhspval3  43258  ovolval4lem1  43288  ovolval4lem2  43289  smfmullem1  43423  smfmullem2  43424  smfmullem3  43425  afv2ex  43770  suppmptcfin  44781  linc1  44834  lcoss  44845  el0ldep  44875