Theorem ifcld 4575

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

Syntax hints:   → wi 4   ∈ wcel 2107  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  ifexd  4577  soltmin  6138  pw2f1olem  9076  unxpdomlem3  9252  wemaplem2  9542  cantnfp1lem1  9673  cantnfp1lem2  9674  cantnfp1lem3  9675  cantnflem1d  9683  cantnflem1  9684  ssfzunsnext  13546  relexpsucnnr  14972  rexuzre  15299  rexico  15300  limsupgre  15425  rlim3  15442  o1lo1  15481  rlimclim1  15489  lo1resb  15508  o1resb  15510  o1of2  15557  o1rlimmul  15563  lo1le  15598  ruclem1  16174  ruclem10  16182  bitsfzo  16376  ramub1lem2  16960  ramcl  16962  prmocl  16967  prmop1  16971  prmdvdsprmo  16975  prmolefac  16979  prmodvdslcmf  16980  prmgapprmo  16995  setsstruct2  17107  wunress  17195  wunressOLD  17196  opifismgm  18578  mulgfval  18952  frgpuptf  19638  gsumzsplit  19795  gsummpt1n0  19833  xrsds  20988  uvcvvcl2  21343  uvcff  21346  snifpsrbag  21475  psr1cl  21522  subrgpsr  21539  mvrf  21544  mplmon  21590  mplmonmul  21591  mplcoe1  21592  evlslem3  21643  evlslem1  21645  coe1tmfv2  21797  gsummoncoe1  21828  mamumat1cl  21941  dmatmulcl  22002  scmatscmiddistr  22010  1mavmul  22050  marrepeval  22065  marrepcl  22066  marepveval  22070  marepvcl  22071  mdetrsca2  22106  mdetr0  22107  mdetrlin2  22109  mdetralt2  22111  mdetero  22112  mdetunilem2  22115  mdetunilem5  22118  mdetunilem6  22119  mdetunilem8  22121  mdetunilem9  22122  maducoeval2  22142  maduf  22143  madutpos  22144  madugsum  22145  gsummatr01lem3  22159  marep01ma  22162  smadiadetglem2  22174  monmatcollpw  22281  pmatcollpw3fi1lem1  22288  pmatcollpw3fi1lem2  22289  xkopt  23159  tsmssplit  23656  ssblex  23934  stdbdxmet  24024  stdbdmet  24025  stdbdbl  24026  stdbdmopn  24027  nlmvscnlem1  24203  tgioo  24312  xrsxmet  24325  icccmplem2  24339  ipcnlem1  24762  ivthlem2  24969  ovolicc2lem5  25038  ioombl1lem1  25075  ioombl1lem3  25077  ioombl1lem4  25078  mbfmax  25166  i1fres  25223  itg1climres  25232  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  limcres  25403  dvferm1lem  25501  dvferm2lem  25503  dvlip2  25512  lhop1  25531  dvfsumrlim  25548  mdegaddle  25592  deg1addle2  25620  deg1sublt  25628  ply1divmo  25653  plyaddlem1  25727  plyaddlem  25729  coeaddlem  25763  dgradd2  25782  plydiveu  25811  abelthlem9  25952  logcnlem2  26151  logcnlem3  26152  cxpcn3lem  26255  lgamgulmlem4  26536  lgamgulmlem6  26538  ftalem2  26578  gausslemma2dlem4  26872  chebbnd1lem1  26972  dchrisumlem3  26994  dchrvmasumiflem1  27004  ostth3  27141  axlowdimlem15  28214  elrspunsn  32547  ply1moneq  32665  dstfrvunirn  33473  circlemeth  33652  indispconn  34225  ex-sategoelel  34412  ex-sategoelelomsuc  34417  knoppndvlem18  35405  itg2addnclem2  36540  itg2addnclem3  36541  ftc1anclem5  36565  sticksstones10  40971  sticksstones12a  40973  metakunt3  40987  metakunt4  40988  metakunt29  41013  metakunt30  41014  metakunt32  41016  metakunt33  41017  rhmmpl  41125  evlsbagval  41138  selvvvval  41157  fsuppind  41162  fsuppssind  41165  mhpind  41166  dffltz  41376  irrapxlem4  41563  irrapxlem5  41564  kelac1  41805  areaquad  41965  cantnfresb  42074  sqrtcval  42392  clsk1indlem4  42795  mnringmulrcld  42987  refsum2cnlem1  43721  rexabslelem  44128  uzublem  44140  ioondisj2  44206  ioondisj1  44207  uzubioo  44280  mullimc  44332  mullimcf  44339  lptioo2  44347  limcleqr  44360  0ellimcdiv  44365  limsupubuzlem  44428  limsupequzmptlem  44444  climxrre  44466  limsup10exlem  44488  limsup10ex  44489  liminf10ex  44490  liminflelimsuplem  44491  icccncfext  44603  cncfiooicclem1  44609  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  stoweid  44779  fourierdlem9  44832  fourierdlem10  44833  fourierdlem37  44860  fourierdlem40  44863  fourierdlem66  44888  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem78  44900  fourierdlem79  44901  fourierdlem95  44917  fourierdlem103  44925  sqwvfoura  44944  fouriersw  44947  etransclem1  44951  etransclem4  44954  etransclem17  44967  etransclem18  44968  etransclem19  44969  etransclem20  44970  etransclem21  44971  etransclem22  44972  etransclem23  44973  etransclem27  44977  etransclem32  44982  etransclem35  44985  etransclem46  44996  ioorrnopnlem  45020  ovnval2  45261  volicorecl  45262  hoiprodcl  45263  ovnf  45279  hsphoif  45292  hsphoival  45295  hoiprodcl3  45296  volicore  45297  hoidmvcl  45298  hsphoidmvle2  45301  hsphoidmvle  45302  hoidmv1lelem1  45307  hoidmv1lelem2  45308  hoidmv1lelem3  45309  hoidmvlelem2  45312  hoidmvlelem3  45313  ovnhoilem1  45317  hoidifhspf  45334  hoidifhspval3  45335  ovolval4lem1  45365  ovolval4lem2  45366  smfmullem1  45507  smfmullem2  45508  smfmullem3  45509  afv2ex  45922  suppmptcfin  47055  linc1  47106  lcoss  47117  el0ldep  47147