Theorem ifcld 4572

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

Syntax hints:   → wi 4   ∈ wcel 2108  ifcif 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  ifexd  4574  soltmin  6156  pw2f1olem  9116  unxpdomlem3  9288  wemaplem2  9587  cantnfp1lem1  9718  cantnfp1lem2  9719  cantnfp1lem3  9720  cantnflem1d  9728  cantnflem1  9729  ssfzunsnext  13609  tpf  14538  relexpsucnnr  15064  rexuzre  15391  rexico  15392  limsupgre  15517  rlim3  15534  o1lo1  15573  rlimclim1  15581  lo1resb  15600  o1resb  15602  o1of2  15649  o1rlimmul  15655  lo1le  15688  ruclem1  16267  ruclem10  16275  bitsfzo  16472  ramub1lem2  17065  ramcl  17067  prmocl  17072  prmop1  17076  prmdvdsprmo  17080  prmolefac  17084  prmodvdslcmf  17085  prmgapprmo  17100  setsstruct2  17211  wunress  17295  wunressOLD  17296  opifismgm  18672  mulgfval  19087  frgpuptf  19788  gsumzsplit  19945  gsummpt1n0  19983  xrsds  21427  uvcvvcl2  21808  uvcff  21811  snifpsrbag  21940  psr1cl  21981  subrgpsr  21998  mvrf  22005  mplmon  22053  mplmonmul  22054  mplcoe1  22055  evlslem3  22104  evlslem1  22106  coe1tmfv2  22278  gsummoncoe1  22312  rhmmpl  22387  rhmply1vr1  22391  mamumat1cl  22445  dmatmulcl  22506  scmatscmiddistr  22514  1mavmul  22554  marrepeval  22569  marrepcl  22570  marepveval  22574  marepvcl  22575  mdetrsca2  22610  mdetr0  22611  mdetrlin2  22613  mdetralt2  22615  mdetero  22616  mdetunilem2  22619  mdetunilem5  22622  mdetunilem6  22623  mdetunilem8  22625  mdetunilem9  22626  maducoeval2  22646  maduf  22647  madutpos  22648  madugsum  22649  gsummatr01lem3  22663  marep01ma  22666  smadiadetglem2  22678  monmatcollpw  22785  pmatcollpw3fi1lem1  22792  pmatcollpw3fi1lem2  22793  xkopt  23663  tsmssplit  24160  ssblex  24438  stdbdxmet  24528  stdbdmet  24529  stdbdbl  24530  stdbdmopn  24531  nlmvscnlem1  24707  tgioo  24817  xrsxmet  24831  icccmplem2  24845  ipcnlem1  25279  ivthlem2  25487  ovolicc2lem5  25556  ioombl1lem1  25593  ioombl1lem3  25595  ioombl1lem4  25596  mbfmax  25684  i1fres  25740  itg1climres  25749  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  limcres  25921  dvferm1lem  26022  dvferm2lem  26024  dvlip2  26034  lhop1  26053  dvfsumrlim  26072  mdegaddle  26113  deg1addle2  26141  deg1sublt  26149  ply1divmo  26175  plyaddlem1  26252  plyaddlem  26254  coeaddlem  26288  dgradd2  26308  plydiveu  26340  abelthlem9  26484  logcnlem2  26685  logcnlem3  26686  cxpcn3lem  26790  lgamgulmlem4  27075  lgamgulmlem6  27077  ftalem2  27117  gausslemma2dlem4  27413  chebbnd1lem1  27513  dchrisumlem3  27535  dchrvmasumiflem1  27545  ostth3  27682  abssval  28263  absscl  28264  axlowdimlem15  28971  elrspunsn  33457  ply1moneq  33611  deg1addlt  33620  fldextrspunlsp  33724  dstfrvunirn  34477  circlemeth  34655  indispconn  35239  ex-sategoelel  35426  ex-sategoelelomsuc  35431  knoppndvlem18  36530  itg2addnclem2  37679  itg2addnclem3  37680  ftc1anclem5  37704  sticksstones10  42156  sticksstones12a  42158  aks6d1c6lem3  42173  metakunt3  42208  metakunt4  42209  metakunt29  42234  metakunt30  42235  metakunt32  42237  metakunt33  42238  rhmpsr  42562  evlsbagval  42576  selvvvval  42595  fsuppind  42600  fsuppssind  42603  mhpind  42604  dffltz  42644  irrapxlem4  42836  irrapxlem5  42837  kelac1  43075  areaquad  43228  cantnfresb  43337  sqrtcval  43654  clsk1indlem4  44057  mnringmulrcld  44247  refsum2cnlem1  45042  rexabslelem  45429  uzublem  45441  ioondisj2  45506  ioondisj1  45507  uzubioo  45580  mullimc  45631  mullimcf  45638  lptioo2  45646  limcleqr  45659  0ellimcdiv  45664  limsupubuzlem  45727  limsupequzmptlem  45743  climxrre  45765  limsup10exlem  45787  limsup10ex  45788  liminf10ex  45789  liminflelimsuplem  45790  icccncfext  45902  cncfiooicclem1  45908  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  stoweid  46078  fourierdlem9  46131  fourierdlem10  46132  fourierdlem37  46159  fourierdlem40  46162  fourierdlem66  46187  fourierdlem73  46194  fourierdlem74  46195  fourierdlem75  46196  fourierdlem78  46199  fourierdlem79  46200  fourierdlem95  46216  fourierdlem103  46224  sqwvfoura  46243  fouriersw  46246  etransclem1  46250  etransclem4  46253  etransclem17  46266  etransclem18  46267  etransclem19  46268  etransclem20  46269  etransclem21  46270  etransclem22  46271  etransclem23  46272  etransclem27  46276  etransclem32  46281  etransclem35  46284  etransclem46  46295  ioorrnopnlem  46319  ovnval2  46560  volicorecl  46561  hoiprodcl  46562  ovnf  46578  hsphoif  46591  hsphoival  46594  hoiprodcl3  46595  volicore  46596  hoidmvcl  46597  hsphoidmvle2  46600  hsphoidmvle  46601  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmvlelem2  46611  hoidmvlelem3  46612  ovnhoilem1  46616  hoidifhspf  46633  hoidifhspval3  46634  ovolval4lem1  46664  ovolval4lem2  46665  smfmullem1  46806  smfmullem2  46807  smfmullem3  46808  afv2ex  47226  suppmptcfin  48292  linc1  48342  lcoss  48353  el0ldep  48383