Theorem ifcld 4547

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

Syntax hints:   → wi 4   ∈ wcel 2108  ifcif 4500

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  ifexd  4549  soltmin  6125  pw2f1olem  9090  unxpdomlem3  9260  wemaplem2  9561  cantnfp1lem1  9692  cantnfp1lem2  9693  cantnfp1lem3  9694  cantnflem1d  9702  cantnflem1  9703  ssfzunsnext  13586  tpf  14517  relexpsucnnr  15044  rexuzre  15371  rexico  15372  limsupgre  15497  rlim3  15514  o1lo1  15553  rlimclim1  15561  lo1resb  15580  o1resb  15582  o1of2  15629  o1rlimmul  15635  lo1le  15668  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  17270  opifismgm  18637  mulgfval  19052  frgpuptf  19751  gsumzsplit  19908  gsummpt1n0  19946  xrsds  21377  uvcvvcl2  21748  uvcff  21751  snifpsrbag  21880  psr1cl  21921  subrgpsr  21938  mvrf  21945  mplmon  21993  mplmonmul  21994  mplcoe1  21995  evlslem3  22038  evlslem1  22040  coe1tmfv2  22212  gsummoncoe1  22246  rhmmpl  22321  rhmply1vr1  22325  mamumat1cl  22377  dmatmulcl  22438  scmatscmiddistr  22446  1mavmul  22486  marrepeval  22501  marrepcl  22502  marepveval  22506  marepvcl  22507  mdetrsca2  22542  mdetr0  22543  mdetrlin2  22545  mdetralt2  22547  mdetero  22548  mdetunilem2  22551  mdetunilem5  22554  mdetunilem6  22555  mdetunilem8  22557  mdetunilem9  22558  maducoeval2  22578  maduf  22579  madutpos  22580  madugsum  22581  gsummatr01lem3  22595  marep01ma  22598  smadiadetglem2  22610  monmatcollpw  22717  pmatcollpw3fi1lem1  22724  pmatcollpw3fi1lem2  22725  xkopt  23593  tsmssplit  24090  ssblex  24367  stdbdxmet  24454  stdbdmet  24455  stdbdbl  24456  stdbdmopn  24457  nlmvscnlem1  24625  tgioo  24735  xrsxmet  24749  icccmplem2  24763  ipcnlem1  25197  ivthlem2  25405  ovolicc2lem5  25474  ioombl1lem1  25511  ioombl1lem3  25513  ioombl1lem4  25514  mbfmax  25602  i1fres  25658  itg1climres  25667  mbfi1fseqlem3  25670  mbfi1fseqlem4  25671  mbfi1fseqlem5  25672  limcres  25839  dvferm1lem  25940  dvferm2lem  25942  dvlip2  25952  lhop1  25971  dvfsumrlim  25990  mdegaddle  26031  deg1addle2  26059  deg1sublt  26067  ply1divmo  26093  plyaddlem1  26170  plyaddlem  26172  coeaddlem  26206  dgradd2  26226  plydiveu  26258  abelthlem9  26402  logcnlem2  26604  logcnlem3  26605  cxpcn3lem  26709  lgamgulmlem4  26994  lgamgulmlem6  26996  ftalem2  27036  gausslemma2dlem4  27332  chebbnd1lem1  27432  dchrisumlem3  27454  dchrvmasumiflem1  27464  ostth3  27601  abssval  28193  absscl  28194  axlowdimlem15  28935  elrspunsn  33444  ply1moneq  33599  deg1addlt  33609  fldextrspunlsp  33715  dstfrvunirn  34507  circlemeth  34672  indispconn  35256  ex-sategoelel  35443  ex-sategoelelomsuc  35448  knoppndvlem18  36547  itg2addnclem2  37696  itg2addnclem3  37697  ftc1anclem5  37721  sticksstones10  42168  sticksstones12a  42170  aks6d1c6lem3  42185  metakunt3  42220  metakunt4  42221  metakunt29  42246  metakunt30  42247  metakunt32  42249  metakunt33  42250  rhmpsr  42575  evlsbagval  42589  selvvvval  42608  fsuppind  42613  fsuppssind  42616  mhpind  42617  dffltz  42657  irrapxlem4  42848  irrapxlem5  42849  kelac1  43087  areaquad  43240  cantnfresb  43348  sqrtcval  43665  clsk1indlem4  44068  mnringmulrcld  44252  refsum2cnlem1  45061  rexabslelem  45445  uzublem  45457  ioondisj2  45522  ioondisj1  45523  uzubioo  45594  mullimc  45645  mullimcf  45652  lptioo2  45660  limcleqr  45673  0ellimcdiv  45678  limsupubuzlem  45741  limsupequzmptlem  45757  climxrre  45779  limsup10exlem  45801  limsup10ex  45802  liminf10ex  45803  liminflelimsuplem  45804  icccncfext  45916  cncfiooicclem1  45922  ioodvbdlimc1lem2  45961  ioodvbdlimc2lem  45963  stoweid  46092  fourierdlem9  46145  fourierdlem10  46146  fourierdlem37  46173  fourierdlem40  46176  fourierdlem66  46201  fourierdlem73  46208  fourierdlem74  46209  fourierdlem75  46210  fourierdlem78  46213  fourierdlem79  46214  fourierdlem95  46230  fourierdlem103  46238  sqwvfoura  46257  fouriersw  46260  etransclem1  46264  etransclem4  46267  etransclem17  46280  etransclem18  46281  etransclem19  46282  etransclem20  46283  etransclem21  46284  etransclem22  46285  etransclem23  46286  etransclem27  46290  etransclem32  46295  etransclem35  46298  etransclem46  46309  ioorrnopnlem  46333  ovnval2  46574  volicorecl  46575  hoiprodcl  46576  ovnf  46592  hsphoif  46605  hsphoival  46608  hoiprodcl3  46609  volicore  46610  hoidmvcl  46611  hsphoidmvle2  46614  hsphoidmvle  46615  hoidmv1lelem1  46620  hoidmv1lelem2  46621  hoidmv1lelem3  46622  hoidmvlelem2  46625  hoidmvlelem3  46626  ovnhoilem1  46630  hoidifhspf  46647  hoidifhspval3  46648  ovolval4lem1  46678  ovolval4lem2  46679  smfmullem1  46820  smfmullem2  46821  smfmullem3  46822  afv2ex  47243  suppmptcfin  48351  linc1  48401  lcoss  48412  el0ldep  48442