Theorem ifcld 4552

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

Syntax hints:   → wi 4   ∈ wcel 2107  ifcif 4505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-if 4506

This theorem is referenced by:  ifexd  4554  soltmin  6136  pw2f1olem  9098  unxpdomlem3  9270  wemaplem2  9569  cantnfp1lem1  9700  cantnfp1lem2  9701  cantnfp1lem3  9702  cantnflem1d  9710  cantnflem1  9711  ssfzunsnext  13591  tpf  14520  relexpsucnnr  15046  rexuzre  15373  rexico  15374  limsupgre  15499  rlim3  15516  o1lo1  15555  rlimclim1  15563  lo1resb  15582  o1resb  15584  o1of2  15631  o1rlimmul  15637  lo1le  15670  ruclem1  16249  ruclem10  16257  bitsfzo  16454  ramub1lem2  17047  ramcl  17049  prmocl  17054  prmop1  17058  prmdvdsprmo  17062  prmolefac  17066  prmodvdslcmf  17067  prmgapprmo  17082  setsstruct2  17193  wunress  17272  opifismgm  18641  mulgfval  19056  frgpuptf  19756  gsumzsplit  19913  gsummpt1n0  19951  xrsds  21389  uvcvvcl2  21762  uvcff  21765  snifpsrbag  21894  psr1cl  21935  subrgpsr  21952  mvrf  21959  mplmon  22007  mplmonmul  22008  mplcoe1  22009  evlslem3  22052  evlslem1  22054  coe1tmfv2  22226  gsummoncoe1  22260  rhmmpl  22335  rhmply1vr1  22339  mamumat1cl  22393  dmatmulcl  22454  scmatscmiddistr  22462  1mavmul  22502  marrepeval  22517  marrepcl  22518  marepveval  22522  marepvcl  22523  mdetrsca2  22558  mdetr0  22559  mdetrlin2  22561  mdetralt2  22563  mdetero  22564  mdetunilem2  22567  mdetunilem5  22570  mdetunilem6  22571  mdetunilem8  22573  mdetunilem9  22574  maducoeval2  22594  maduf  22595  madutpos  22596  madugsum  22597  gsummatr01lem3  22611  marep01ma  22614  smadiadetglem2  22626  monmatcollpw  22733  pmatcollpw3fi1lem1  22740  pmatcollpw3fi1lem2  22741  xkopt  23609  tsmssplit  24106  ssblex  24383  stdbdxmet  24472  stdbdmet  24473  stdbdbl  24474  stdbdmopn  24475  nlmvscnlem1  24643  tgioo  24753  xrsxmet  24767  icccmplem2  24781  ipcnlem1  25215  ivthlem2  25423  ovolicc2lem5  25492  ioombl1lem1  25529  ioombl1lem3  25531  ioombl1lem4  25532  mbfmax  25620  i1fres  25676  itg1climres  25685  mbfi1fseqlem3  25688  mbfi1fseqlem4  25689  mbfi1fseqlem5  25690  limcres  25857  dvferm1lem  25958  dvferm2lem  25960  dvlip2  25970  lhop1  25989  dvfsumrlim  26008  mdegaddle  26049  deg1addle2  26077  deg1sublt  26085  ply1divmo  26111  plyaddlem1  26188  plyaddlem  26190  coeaddlem  26224  dgradd2  26244  plydiveu  26276  abelthlem9  26420  logcnlem2  26621  logcnlem3  26622  cxpcn3lem  26726  lgamgulmlem4  27011  lgamgulmlem6  27013  ftalem2  27053  gausslemma2dlem4  27349  chebbnd1lem1  27449  dchrisumlem3  27471  dchrvmasumiflem1  27481  ostth3  27618  abssval  28199  absscl  28200  axlowdimlem15  28901  elrspunsn  33392  ply1moneq  33546  deg1addlt  33555  fldextrspunlsp  33661  dstfrvunirn  34436  circlemeth  34614  indispconn  35198  ex-sategoelel  35385  ex-sategoelelomsuc  35390  knoppndvlem18  36489  itg2addnclem2  37638  itg2addnclem3  37639  ftc1anclem5  37663  sticksstones10  42115  sticksstones12a  42117  aks6d1c6lem3  42132  metakunt3  42167  metakunt4  42168  metakunt29  42193  metakunt30  42194  metakunt32  42196  metakunt33  42197  rhmpsr  42525  evlsbagval  42539  selvvvval  42558  fsuppind  42563  fsuppssind  42566  mhpind  42567  dffltz  42607  irrapxlem4  42799  irrapxlem5  42800  kelac1  43038  areaquad  43191  cantnfresb  43299  sqrtcval  43616  clsk1indlem4  44019  mnringmulrcld  44204  refsum2cnlem1  44999  rexabslelem  45386  uzublem  45398  ioondisj2  45463  ioondisj1  45464  uzubioo  45537  mullimc  45588  mullimcf  45595  lptioo2  45603  limcleqr  45616  0ellimcdiv  45621  limsupubuzlem  45684  limsupequzmptlem  45700  climxrre  45722  limsup10exlem  45744  limsup10ex  45745  liminf10ex  45746  liminflelimsuplem  45747  icccncfext  45859  cncfiooicclem1  45865  ioodvbdlimc1lem2  45904  ioodvbdlimc2lem  45906  stoweid  46035  fourierdlem9  46088  fourierdlem10  46089  fourierdlem37  46116  fourierdlem40  46119  fourierdlem66  46144  fourierdlem73  46151  fourierdlem74  46152  fourierdlem75  46153  fourierdlem78  46156  fourierdlem79  46157  fourierdlem95  46173  fourierdlem103  46181  sqwvfoura  46200  fouriersw  46203  etransclem1  46207  etransclem4  46210  etransclem17  46223  etransclem18  46224  etransclem19  46225  etransclem20  46226  etransclem21  46227  etransclem22  46228  etransclem23  46229  etransclem27  46233  etransclem32  46238  etransclem35  46241  etransclem46  46252  ioorrnopnlem  46276  ovnval2  46517  volicorecl  46518  hoiprodcl  46519  ovnf  46535  hsphoif  46548  hsphoival  46551  hoiprodcl3  46552  volicore  46553  hoidmvcl  46554  hsphoidmvle2  46557  hsphoidmvle  46558  hoidmv1lelem1  46563  hoidmv1lelem2  46564  hoidmv1lelem3  46565  hoidmvlelem2  46568  hoidmvlelem3  46569  ovnhoilem1  46573  hoidifhspf  46590  hoidifhspval3  46591  ovolval4lem1  46621  ovolval4lem2  46622  smfmullem1  46763  smfmullem2  46764  smfmullem3  46765  afv2ex  47184  suppmptcfin  48250  linc1  48300  lcoss  48311  el0ldep  48341