Theorem ifcld 4527

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

Syntax hints:   → wi 4   ∈ wcel 2114  ifcif 4480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4481

This theorem is referenced by:  ifexd  4529  soltmin  6094  pw2f1olem  9013  unxpdomlem3  9162  wemaplem2  9456  cantnfp1lem1  9591  cantnfp1lem2  9592  cantnfp1lem3  9593  cantnflem1d  9601  cantnflem1  9602  ssfzunsnext  13489  tpf  14426  relexpsucnnr  14952  rexuzre  15280  rexico  15281  limsupgre  15408  rlim3  15425  o1lo1  15464  rlimclim1  15472  lo1resb  15491  o1resb  15493  o1of2  15540  o1rlimmul  15546  lo1le  15579  ruclem1  16160  ruclem10  16168  bitsfzo  16366  ramub1lem2  16959  ramcl  16961  prmocl  16966  prmop1  16970  prmdvdsprmo  16974  prmolefac  16978  prmodvdslcmf  16979  prmgapprmo  16994  setsstruct2  17105  wunress  17180  opifismgm  18588  mulgfval  19003  frgpuptf  19703  gsumzsplit  19860  gsummpt1n0  19898  xrsds  21368  uvcvvcl2  21747  uvcff  21750  snifpsrbag  21880  psr1cl  21920  subrgpsr  21937  mvrf  21944  mplmon  21994  mplmonmul  21995  mplcoe1  21996  evlslem3  22039  evlslem1  22041  coe1tmfv2  22221  gsummoncoe1  22256  rhmmpl  22331  rhmply1vr1  22335  mamumat1cl  22387  dmatmulcl  22448  scmatscmiddistr  22456  1mavmul  22496  marrepeval  22511  marrepcl  22512  marepveval  22516  marepvcl  22517  mdetrsca2  22552  mdetr0  22553  mdetrlin2  22555  mdetralt2  22557  mdetero  22558  mdetunilem2  22561  mdetunilem5  22564  mdetunilem6  22565  mdetunilem8  22567  mdetunilem9  22568  maducoeval2  22588  maduf  22589  madutpos  22590  madugsum  22591  gsummatr01lem3  22605  marep01ma  22608  smadiadetglem2  22620  monmatcollpw  22727  pmatcollpw3fi1lem1  22734  pmatcollpw3fi1lem2  22735  xkopt  23603  tsmssplit  24100  ssblex  24376  stdbdxmet  24463  stdbdmet  24464  stdbdbl  24465  stdbdmopn  24466  nlmvscnlem1  24634  tgioo  24744  xrsxmet  24758  icccmplem2  24772  ipcnlem1  25205  ivthlem2  25413  ovolicc2lem5  25482  ioombl1lem1  25519  ioombl1lem3  25521  ioombl1lem4  25522  mbfmax  25610  i1fres  25666  itg1climres  25675  mbfi1fseqlem3  25678  mbfi1fseqlem4  25679  mbfi1fseqlem5  25680  limcres  25847  dvferm1lem  25948  dvferm2lem  25950  dvlip2  25960  lhop1  25979  dvfsumrlim  25998  mdegaddle  26039  deg1addle2  26067  deg1sublt  26075  ply1divmo  26101  plyaddlem1  26178  plyaddlem  26180  coeaddlem  26214  dgradd2  26234  plydiveu  26266  abelthlem9  26410  logcnlem2  26612  logcnlem3  26613  cxpcn3lem  26717  lgamgulmlem4  27002  lgamgulmlem6  27004  ftalem2  27044  gausslemma2dlem4  27340  chebbnd1lem1  27440  dchrisumlem3  27462  dchrvmasumiflem1  27472  ostth3  27609  abssval  28239  absscl  28240  axlowdimlem15  29033  elrspunsn  33512  ply1moneq  33671  deg1addlt  33683  extvfvv  33701  extvfvvcl  33702  extvfvcl  33703  mplvrpmrhm  33714  esplyfval0  33724  esplyind  33733  fldextrspunlsp  33833  dstfrvunirn  34634  circlemeth  34799  indispconn  35430  ex-sategoelel  35617  ex-sategoelelomsuc  35622  knoppndvlem18  36731  itg2addnclem2  37875  itg2addnclem3  37876  ftc1anclem5  37900  sticksstones10  42477  sticksstones12a  42479  aks6d1c6lem3  42494  rhmpsr  42872  evlsbagval  42879  selvvvval  42895  fsuppind  42900  fsuppssind  42903  mhpind  42904  dffltz  42944  irrapxlem4  43134  irrapxlem5  43135  kelac1  43372  areaquad  43525  cantnfresb  43633  sqrtcval  43949  clsk1indlem4  44352  mnringmulrcld  44536  refsum2cnlem1  45349  rexabslelem  45729  uzublem  45741  ioondisj2  45806  ioondisj1  45807  uzubioo  45878  mullimc  45929  mullimcf  45936  lptioo2  45944  limcleqr  45955  0ellimcdiv  45960  limsupubuzlem  46023  limsupequzmptlem  46039  climxrre  46061  limsup10exlem  46083  limsup10ex  46084  liminf10ex  46085  liminflelimsuplem  46086  icccncfext  46198  cncfiooicclem1  46204  ioodvbdlimc1lem2  46243  ioodvbdlimc2lem  46245  stoweid  46374  fourierdlem9  46427  fourierdlem10  46428  fourierdlem37  46455  fourierdlem40  46458  fourierdlem66  46483  fourierdlem73  46490  fourierdlem74  46491  fourierdlem75  46492  fourierdlem78  46495  fourierdlem79  46496  fourierdlem95  46512  fourierdlem103  46520  sqwvfoura  46539  fouriersw  46542  etransclem1  46546  etransclem4  46549  etransclem17  46562  etransclem18  46563  etransclem19  46564  etransclem20  46565  etransclem21  46566  etransclem22  46567  etransclem23  46568  etransclem27  46572  etransclem32  46577  etransclem35  46580  etransclem46  46591  ioorrnopnlem  46615  ovnval2  46856  volicorecl  46857  hoiprodcl  46858  ovnf  46874  hsphoif  46887  hsphoival  46890  hoiprodcl3  46891  volicore  46892  hoidmvcl  46893  hsphoidmvle2  46896  hsphoidmvle  46897  hoidmv1lelem1  46902  hoidmv1lelem2  46903  hoidmv1lelem3  46904  hoidmvlelem2  46907  hoidmvlelem3  46908  ovnhoilem1  46912  hoidifhspf  46929  hoidifhspval3  46930  ovolval4lem1  46960  ovolval4lem2  46961  smfmullem1  47102  smfmullem2  47103  smfmullem3  47104  afv2ex  47527  suppmptcfin  48689  linc1  48738  lcoss  48749  el0ldep  48779