Theorem ifcld 4524

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

Syntax hints:   → wi 4   ∈ wcel 2113  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-if 4478

This theorem is referenced by:  ifexd  4526  soltmin  6091  pw2f1olem  9007  unxpdomlem3  9156  wemaplem2  9450  cantnfp1lem1  9585  cantnfp1lem2  9586  cantnfp1lem3  9587  cantnflem1d  9595  cantnflem1  9596  ssfzunsnext  13483  tpf  14420  relexpsucnnr  14946  rexuzre  15274  rexico  15275  limsupgre  15402  rlim3  15419  o1lo1  15458  rlimclim1  15466  lo1resb  15485  o1resb  15487  o1of2  15534  o1rlimmul  15540  lo1le  15573  ruclem1  16154  ruclem10  16162  bitsfzo  16360  ramub1lem2  16953  ramcl  16955  prmocl  16960  prmop1  16964  prmdvdsprmo  16968  prmolefac  16972  prmodvdslcmf  16973  prmgapprmo  16988  setsstruct2  17099  wunress  17174  opifismgm  18582  mulgfval  18997  frgpuptf  19697  gsumzsplit  19854  gsummpt1n0  19892  xrsds  21362  uvcvvcl2  21741  uvcff  21744  snifpsrbag  21874  psr1cl  21914  subrgpsr  21931  mvrf  21938  mplmon  21988  mplmonmul  21989  mplcoe1  21990  evlslem3  22033  evlslem1  22035  coe1tmfv2  22215  gsummoncoe1  22250  rhmmpl  22325  rhmply1vr1  22329  mamumat1cl  22381  dmatmulcl  22442  scmatscmiddistr  22450  1mavmul  22490  marrepeval  22505  marrepcl  22506  marepveval  22510  marepvcl  22511  mdetrsca2  22546  mdetr0  22547  mdetrlin2  22549  mdetralt2  22551  mdetero  22552  mdetunilem2  22555  mdetunilem5  22558  mdetunilem6  22559  mdetunilem8  22561  mdetunilem9  22562  maducoeval2  22582  maduf  22583  madutpos  22584  madugsum  22585  gsummatr01lem3  22599  marep01ma  22602  smadiadetglem2  22614  monmatcollpw  22721  pmatcollpw3fi1lem1  22728  pmatcollpw3fi1lem2  22729  xkopt  23597  tsmssplit  24094  ssblex  24370  stdbdxmet  24457  stdbdmet  24458  stdbdbl  24459  stdbdmopn  24460  nlmvscnlem1  24628  tgioo  24738  xrsxmet  24752  icccmplem2  24766  ipcnlem1  25199  ivthlem2  25407  ovolicc2lem5  25476  ioombl1lem1  25513  ioombl1lem3  25515  ioombl1lem4  25516  mbfmax  25604  i1fres  25660  itg1climres  25669  mbfi1fseqlem3  25672  mbfi1fseqlem4  25673  mbfi1fseqlem5  25674  limcres  25841  dvferm1lem  25942  dvferm2lem  25944  dvlip2  25954  lhop1  25973  dvfsumrlim  25992  mdegaddle  26033  deg1addle2  26061  deg1sublt  26069  ply1divmo  26095  plyaddlem1  26172  plyaddlem  26174  coeaddlem  26208  dgradd2  26228  plydiveu  26260  abelthlem9  26404  logcnlem2  26606  logcnlem3  26607  cxpcn3lem  26711  lgamgulmlem4  26996  lgamgulmlem6  26998  ftalem2  27038  gausslemma2dlem4  27334  chebbnd1lem1  27434  dchrisumlem3  27456  dchrvmasumiflem1  27466  ostth3  27603  abssval  28207  absscl  28208  axlowdimlem15  28978  elrspunsn  33459  ply1moneq  33618  deg1addlt  33630  extvfvv  33648  extvfvvcl  33649  extvfvcl  33650  mplvrpmrhm  33661  esplyfval0  33671  esplyind  33680  fldextrspunlsp  33780  dstfrvunirn  34581  circlemeth  34746  indispconn  35377  ex-sategoelel  35564  ex-sategoelelomsuc  35569  knoppndvlem18  36672  itg2addnclem2  37812  itg2addnclem3  37813  ftc1anclem5  37837  sticksstones10  42348  sticksstones12a  42350  aks6d1c6lem3  42365  rhmpsr  42747  evlsbagval  42754  selvvvval  42770  fsuppind  42775  fsuppssind  42778  mhpind  42779  dffltz  42819  irrapxlem4  43009  irrapxlem5  43010  kelac1  43247  areaquad  43400  cantnfresb  43508  sqrtcval  43824  clsk1indlem4  44227  mnringmulrcld  44411  refsum2cnlem1  45224  rexabslelem  45604  uzublem  45616  ioondisj2  45681  ioondisj1  45682  uzubioo  45753  mullimc  45804  mullimcf  45811  lptioo2  45819  limcleqr  45830  0ellimcdiv  45835  limsupubuzlem  45898  limsupequzmptlem  45914  climxrre  45936  limsup10exlem  45958  limsup10ex  45959  liminf10ex  45960  liminflelimsuplem  45961  icccncfext  46073  cncfiooicclem1  46079  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  stoweid  46249  fourierdlem9  46302  fourierdlem10  46303  fourierdlem37  46330  fourierdlem40  46333  fourierdlem66  46358  fourierdlem73  46365  fourierdlem74  46366  fourierdlem75  46367  fourierdlem78  46370  fourierdlem79  46371  fourierdlem95  46387  fourierdlem103  46395  sqwvfoura  46414  fouriersw  46417  etransclem1  46421  etransclem4  46424  etransclem17  46437  etransclem18  46438  etransclem19  46439  etransclem20  46440  etransclem21  46441  etransclem22  46442  etransclem23  46443  etransclem27  46447  etransclem32  46452  etransclem35  46455  etransclem46  46466  ioorrnopnlem  46490  ovnval2  46731  volicorecl  46732  hoiprodcl  46733  ovnf  46749  hsphoif  46762  hsphoival  46765  hoiprodcl3  46766  volicore  46767  hoidmvcl  46768  hsphoidmvle2  46771  hsphoidmvle  46772  hoidmv1lelem1  46777  hoidmv1lelem2  46778  hoidmv1lelem3  46779  hoidmvlelem2  46782  hoidmvlelem3  46783  ovnhoilem1  46787  hoidifhspf  46804  hoidifhspval3  46805  ovolval4lem1  46835  ovolval4lem2  46836  smfmullem1  46977  smfmullem2  46978  smfmullem3  46979  afv2ex  47402  suppmptcfin  48564  linc1  48613  lcoss  48624  el0ldep  48654