Theorem ifcld 4519

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

Syntax hints:   → wi 4   ∈ wcel 2111  ifcif 4472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4473

This theorem is referenced by:  ifexd  4521  soltmin  6082  pw2f1olem  8994  unxpdomlem3  9142  wemaplem2  9433  cantnfp1lem1  9568  cantnfp1lem2  9569  cantnfp1lem3  9570  cantnflem1d  9578  cantnflem1  9579  ssfzunsnext  13469  tpf  14406  relexpsucnnr  14932  rexuzre  15260  rexico  15261  limsupgre  15388  rlim3  15405  o1lo1  15444  rlimclim1  15452  lo1resb  15471  o1resb  15473  o1of2  15520  o1rlimmul  15526  lo1le  15559  ruclem1  16140  ruclem10  16148  bitsfzo  16346  ramub1lem2  16939  ramcl  16941  prmocl  16946  prmop1  16950  prmdvdsprmo  16954  prmolefac  16958  prmodvdslcmf  16959  prmgapprmo  16974  setsstruct2  17085  wunress  17160  opifismgm  18567  mulgfval  18982  frgpuptf  19682  gsumzsplit  19839  gsummpt1n0  19877  xrsds  21346  uvcvvcl2  21725  uvcff  21728  snifpsrbag  21857  psr1cl  21898  subrgpsr  21915  mvrf  21922  mplmon  21970  mplmonmul  21971  mplcoe1  21972  evlslem3  22015  evlslem1  22017  coe1tmfv2  22189  gsummoncoe1  22223  rhmmpl  22298  rhmply1vr1  22302  mamumat1cl  22354  dmatmulcl  22415  scmatscmiddistr  22423  1mavmul  22463  marrepeval  22478  marrepcl  22479  marepveval  22483  marepvcl  22484  mdetrsca2  22519  mdetr0  22520  mdetrlin2  22522  mdetralt2  22524  mdetero  22525  mdetunilem2  22528  mdetunilem5  22531  mdetunilem6  22532  mdetunilem8  22534  mdetunilem9  22535  maducoeval2  22555  maduf  22556  madutpos  22557  madugsum  22558  gsummatr01lem3  22572  marep01ma  22575  smadiadetglem2  22587  monmatcollpw  22694  pmatcollpw3fi1lem1  22701  pmatcollpw3fi1lem2  22702  xkopt  23570  tsmssplit  24067  ssblex  24343  stdbdxmet  24430  stdbdmet  24431  stdbdbl  24432  stdbdmopn  24433  nlmvscnlem1  24601  tgioo  24711  xrsxmet  24725  icccmplem2  24739  ipcnlem1  25172  ivthlem2  25380  ovolicc2lem5  25449  ioombl1lem1  25486  ioombl1lem3  25488  ioombl1lem4  25489  mbfmax  25577  i1fres  25633  itg1climres  25642  mbfi1fseqlem3  25645  mbfi1fseqlem4  25646  mbfi1fseqlem5  25647  limcres  25814  dvferm1lem  25915  dvferm2lem  25917  dvlip2  25927  lhop1  25946  dvfsumrlim  25965  mdegaddle  26006  deg1addle2  26034  deg1sublt  26042  ply1divmo  26068  plyaddlem1  26145  plyaddlem  26147  coeaddlem  26181  dgradd2  26201  plydiveu  26233  abelthlem9  26377  logcnlem2  26579  logcnlem3  26580  cxpcn3lem  26684  lgamgulmlem4  26969  lgamgulmlem6  26971  ftalem2  27011  gausslemma2dlem4  27307  chebbnd1lem1  27407  dchrisumlem3  27429  dchrvmasumiflem1  27439  ostth3  27576  abssval  28177  absscl  28178  axlowdimlem15  28934  elrspunsn  33394  ply1moneq  33550  deg1addlt  33560  mplvrpmrhm  33577  fldextrspunlsp  33687  dstfrvunirn  34488  circlemeth  34653  indispconn  35278  ex-sategoelel  35465  ex-sategoelelomsuc  35470  knoppndvlem18  36573  itg2addnclem2  37711  itg2addnclem3  37712  ftc1anclem5  37736  sticksstones10  42247  sticksstones12a  42249  aks6d1c6lem3  42264  rhmpsr  42644  evlsbagval  42658  selvvvval  42677  fsuppind  42682  fsuppssind  42685  mhpind  42686  dffltz  42726  irrapxlem4  42917  irrapxlem5  42918  kelac1  43155  areaquad  43308  cantnfresb  43416  sqrtcval  43733  clsk1indlem4  44136  mnringmulrcld  44320  refsum2cnlem1  45133  rexabslelem  45515  uzublem  45527  ioondisj2  45592  ioondisj1  45593  uzubioo  45664  mullimc  45715  mullimcf  45722  lptioo2  45730  limcleqr  45741  0ellimcdiv  45746  limsupubuzlem  45809  limsupequzmptlem  45825  climxrre  45847  limsup10exlem  45869  limsup10ex  45870  liminf10ex  45871  liminflelimsuplem  45872  icccncfext  45984  cncfiooicclem1  45990  ioodvbdlimc1lem2  46029  ioodvbdlimc2lem  46031  stoweid  46160  fourierdlem9  46213  fourierdlem10  46214  fourierdlem37  46241  fourierdlem40  46244  fourierdlem66  46269  fourierdlem73  46276  fourierdlem74  46277  fourierdlem75  46278  fourierdlem78  46281  fourierdlem79  46282  fourierdlem95  46298  fourierdlem103  46306  sqwvfoura  46325  fouriersw  46328  etransclem1  46332  etransclem4  46335  etransclem17  46348  etransclem18  46349  etransclem19  46350  etransclem20  46351  etransclem21  46352  etransclem22  46353  etransclem23  46354  etransclem27  46358  etransclem32  46363  etransclem35  46366  etransclem46  46377  ioorrnopnlem  46401  ovnval2  46642  volicorecl  46643  hoiprodcl  46644  ovnf  46660  hsphoif  46673  hsphoival  46676  hoiprodcl3  46677  volicore  46678  hoidmvcl  46679  hsphoidmvle2  46682  hsphoidmvle  46683  hoidmv1lelem1  46688  hoidmv1lelem2  46689  hoidmv1lelem3  46690  hoidmvlelem2  46693  hoidmvlelem3  46694  ovnhoilem1  46698  hoidifhspf  46715  hoidifhspval3  46716  ovolval4lem1  46746  ovolval4lem2  46747  smfmullem1  46888  smfmullem2  46889  smfmullem3  46890  afv2ex  47313  suppmptcfin  48475  linc1  48525  lcoss  48536  el0ldep  48566