Theorem ifcld 4532

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  ifexd  4534  soltmin  6136  pw2f1olem  9114  unxpdomlem3  9263  wemaplem2  9554  cantnfp1lem1  9692  cantnfp1lem2  9693  cantnfp1lem3  9694  cantnflem1d  9702  cantnflem1  9703  ssfzunsnext  13716  tpf  14657  relexpsucnnr  15193  rexuzre  15535  rexico  15536  limsupgre  15663  rlim3  15680  o1lo1  15719  rlimclim1  15727  lo1resb  15746  o1resb  15748  o1of2  15795  o1rlimmul  15801  lo1le  15834  ruclem1  16414  ruclem10  16422  bitsfzo  16620  ramub1lem2  17220  ramcl  17222  prmocl  17227  prmop1  17231  prmdvdsprmo  17235  prmolefac  17239  prmodvdslcmf  17240  prmgapprmo  17255  setsstruct2  17367  wunress  17442  opifismgm  18852  mulgfval  19294  frgpuptf  19999  gsumzsplit  20156  gsummpt1n0  20194  xrsds  21731  uvcvvcl2  22109  uvcff  22112  snifpsrbag  22243  psr1cl  22283  subrgpsr  22300  mvrf  22307  mplmon  22359  mplmonmul  22360  mplcoe1  22361  evlslem3  22404  evlslem1  22406  selvvvval  22466  coe1tmfv2  22609  gsummoncoe1  22641  rhmmpl  22713  rhmply1vr1  22717  mamumat1cl  22769  dmatmulcl  22830  scmatscmiddistr  22838  1mavmul  22878  marrepeval  22893  marrepcl  22894  marepveval  22898  marepvcl  22899  mdetrsca2  22934  mdetr0  22935  mdetrlin2  22937  mdetralt2  22939  mdetero  22940  mdetunilem2  22943  mdetunilem5  22946  mdetunilem6  22947  mdetunilem8  22949  mdetunilem9  22950  maducoeval2  22970  maduf  22971  madutpos  22972  madugsum  22973  gsummatr01lem3  22987  marep01ma  22990  smadiadetglem2  23002  monmatcollpw  23112  pmatcollpw3fi1lem1  23119  pmatcollpw3fi1lem2  23120  xkopt  23989  tsmssplit  24486  ssblex  24762  stdbdxmet  24849  stdbdmet  24850  stdbdbl  24851  stdbdmopn  24852  nlmvscnlem1  25020  tgioo  25130  xrsxmet  25144  icccmplem2  25158  ipcnlem1  25581  ivthlem2  25788  ovolicc2lem5  25857  ioombl1lem1  25894  ioombl1lem3  25896  ioombl1lem4  25897  mbfmax  25985  i1fres  26041  itg1climres  26050  mbfi1fseqlem3  26053  mbfi1fseqlem4  26054  mbfi1fseqlem5  26055  limcres  26221  dvferm1lem  26319  dvferm2lem  26321  dvlip2  26330  lhop1  26349  dvfsumrlim  26366  mdegaddle  26407  deg1addle2  26435  deg1sublt  26443  ply1divmo  26469  plyaddlem1  26547  plyaddlem  26549  coeaddlem  26583  dgradd2  26602  plydiveu  26634  abelthlem9  26782  logcnlem2  26986  logcnlem3  26987  cxpcn3lem  27090  lgamgulmlem4  27374  lgamgulmlem6  27376  ftalem2  27416  gausslemma2dlem4  27711  chebbnd1lem1  27811  dchrisumlem3  27833  dchrvmasumiflem1  27843  ostth3  27980  abssval  28640  absscl  28641  axlowdimlem15  29549  elrspunsn  34035  ply1moneq  34176  deg1addlt  34188  mplasclco  34204  selvply1rhmlem2  34209  extvfvv  34222  extvfvvcl  34223  extvfvcl  34224  mplvrpmrhm  34235  psrmon  34237  psrmonmul  34238  psrmonprod  34240  mplmonprod  34242  esplyfval0  34252  esplyfval1  34261  esplyind  34263  fldextrspunlsp  34362  dstfrvunirn  35163  circlemeth  35325  indispconn  36123  ex-sategoelel  36310  ex-sategoelelomsuc  36315  knoppndvlem18  37528  itg2addnclem2  38736  itg2addnclem3  38737  ftc1anclem5  38761  sticksstones10  43351  sticksstones12a  43353  aks6d1c6lem3  43368  rhmpsr  43757  evlsbagval  43760  fsuppind  43764  fsuppssind  43767  mhpind  43768  dffltz  43816  irrapxlem4  43978  irrapxlem5  43979  kelac1  44211  areaquad  44364  cantnfresb  44472  sqrtcval  44787  clsk1indlem4  45190  mnringmulrcld  45372  refsum2cnlem1  46199  rexabslelem  46573  uzublem  46585  ioondisj2  46650  ioondisj1  46651  uzubioo  46722  mullimc  46773  mullimcf  46780  lptioo2  46788  limcleqr  46799  0ellimcdiv  46804  limsupubuzlem  46867  limsupequzmptlem  46883  climxrre  46905  limsup10exlem  46927  limsup10ex  46928  liminf10ex  46929  liminflelimsuplem  46930  icccncfext  47042  cncfiooicclem1  47048  ioodvbdlimc1lem2  47087  ioodvbdlimc2lem  47089  stoweid  47218  fourierdlem9  47271  fourierdlem10  47272  fourierdlem37  47299  fourierdlem40  47302  fourierdlem66  47327  fourierdlem73  47334  fourierdlem74  47335  fourierdlem75  47336  fourierdlem78  47339  fourierdlem79  47340  fourierdlem95  47356  fourierdlem103  47364  sqwvfoura  47383  fouriersw  47386  etransclem1  47390  etransclem4  47393  etransclem17  47406  etransclem18  47407  etransclem19  47408  etransclem20  47409  etransclem21  47410  etransclem22  47411  etransclem23  47412  etransclem27  47416  etransclem32  47421  etransclem35  47424  etransclem46  47435  ioorrnopnlem  47459  ovnval2  47700  volicorecl  47701  hoiprodcl  47702  ovnf  47718  hsphoif  47731  hsphoival  47734  hoiprodcl3  47735  volicore  47736  hoidmvcl  47737  hsphoidmvle2  47740  hsphoidmvle  47741  hoidmv1lelem1  47746  hoidmv1lelem2  47747  hoidmv1lelem3  47748  hoidmvlelem2  47751  hoidmvlelem3  47752  ovnhoilem1  47756  hoidifhspf  47773  hoidifhspval3  47774  ovolval4lem1  47804  ovolval4lem2  47805  smfmullem1  47946  smfmullem2  47947  smfmullem3  47948  tmachlem-agreeprod  48092  tmachlem-tpopen  48096  afv2ex  48429  suppmptcfin  49633  linc1  49682  lcoss  49693  el0ldep  49723  crosspclem  51178  veronesefvcl  51192