Theorem ifcld 4513

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

Syntax hints:   → wi 4   ∈ wcel 2114  ifcif 4466

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  ifexd  4515  soltmin  6099  pw2f1olem  9019  unxpdomlem3  9168  wemaplem2  9462  cantnfp1lem1  9599  cantnfp1lem2  9600  cantnfp1lem3  9601  cantnflem1d  9609  cantnflem1  9610  ssfzunsnext  13523  tpf  14461  relexpsucnnr  14987  rexuzre  15315  rexico  15316  limsupgre  15443  rlim3  15460  o1lo1  15499  rlimclim1  15507  lo1resb  15526  o1resb  15528  o1of2  15575  o1rlimmul  15581  lo1le  15614  ruclem1  16198  ruclem10  16206  bitsfzo  16404  ramub1lem2  16998  ramcl  17000  prmocl  17005  prmop1  17009  prmdvdsprmo  17013  prmolefac  17017  prmodvdslcmf  17018  prmgapprmo  17033  setsstruct2  17144  wunress  17219  opifismgm  18627  mulgfval  19045  frgpuptf  19745  gsumzsplit  19902  gsummpt1n0  19940  xrsds  21390  uvcvvcl2  21768  uvcff  21771  snifpsrbag  21900  psr1cl  21939  subrgpsr  21956  mvrf  21963  mplmon  22013  mplmonmul  22014  mplcoe1  22015  evlslem3  22058  evlslem1  22060  coe1tmfv2  22240  gsummoncoe1  22273  rhmmpl  22348  rhmply1vr1  22352  mamumat1cl  22404  dmatmulcl  22465  scmatscmiddistr  22473  1mavmul  22513  marrepeval  22528  marrepcl  22529  marepveval  22533  marepvcl  22534  mdetrsca2  22569  mdetr0  22570  mdetrlin2  22572  mdetralt2  22574  mdetero  22575  mdetunilem2  22578  mdetunilem5  22581  mdetunilem6  22582  mdetunilem8  22584  mdetunilem9  22585  maducoeval2  22605  maduf  22606  madutpos  22607  madugsum  22608  gsummatr01lem3  22622  marep01ma  22625  smadiadetglem2  22637  monmatcollpw  22744  pmatcollpw3fi1lem1  22751  pmatcollpw3fi1lem2  22752  xkopt  23620  tsmssplit  24117  ssblex  24393  stdbdxmet  24480  stdbdmet  24481  stdbdbl  24482  stdbdmopn  24483  nlmvscnlem1  24651  tgioo  24761  xrsxmet  24775  icccmplem2  24789  ipcnlem1  25212  ivthlem2  25419  ovolicc2lem5  25488  ioombl1lem1  25525  ioombl1lem3  25527  ioombl1lem4  25528  mbfmax  25616  i1fres  25672  itg1climres  25681  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  limcres  25853  dvferm1lem  25951  dvferm2lem  25953  dvlip2  25962  lhop1  25981  dvfsumrlim  25998  mdegaddle  26039  deg1addle2  26067  deg1sublt  26075  ply1divmo  26101  plyaddlem1  26178  plyaddlem  26180  coeaddlem  26214  dgradd2  26233  plydiveu  26264  abelthlem9  26405  logcnlem2  26607  logcnlem3  26608  cxpcn3lem  26711  lgamgulmlem4  26995  lgamgulmlem6  26997  ftalem2  27037  gausslemma2dlem4  27332  chebbnd1lem1  27432  dchrisumlem3  27454  dchrvmasumiflem1  27464  ostth3  27601  abssval  28231  absscl  28232  axlowdimlem15  29025  elrspunsn  33489  ply1moneq  33648  deg1addlt  33660  extvfvv  33678  extvfvvcl  33679  extvfvcl  33680  mplvrpmrhm  33691  psrmon  33693  psrmonmul  33694  psrmonprod  33696  mplmonprod  33698  esplyfval0  33708  esplyfval1  33717  esplyind  33719  fldextrspunlsp  33818  dstfrvunirn  34619  circlemeth  34784  indispconn  35416  ex-sategoelel  35603  ex-sategoelelomsuc  35608  knoppndvlem18  36789  itg2addnclem2  37993  itg2addnclem3  37994  ftc1anclem5  38018  sticksstones10  42594  sticksstones12a  42596  aks6d1c6lem3  42611  rhmpsr  42995  evlsbagval  43002  selvvvval  43018  fsuppind  43023  fsuppssind  43026  mhpind  43027  dffltz  43067  irrapxlem4  43253  irrapxlem5  43254  kelac1  43491  areaquad  43644  cantnfresb  43752  sqrtcval  44068  clsk1indlem4  44471  mnringmulrcld  44655  refsum2cnlem1  45468  rexabslelem  45846  uzublem  45858  ioondisj2  45923  ioondisj1  45924  uzubioo  45995  mullimc  46046  mullimcf  46053  lptioo2  46061  limcleqr  46072  0ellimcdiv  46077  limsupubuzlem  46140  limsupequzmptlem  46156  climxrre  46178  limsup10exlem  46200  limsup10ex  46201  liminf10ex  46202  liminflelimsuplem  46203  icccncfext  46315  cncfiooicclem1  46321  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  stoweid  46491  fourierdlem9  46544  fourierdlem10  46545  fourierdlem37  46572  fourierdlem40  46575  fourierdlem66  46600  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem78  46612  fourierdlem79  46613  fourierdlem95  46629  fourierdlem103  46637  sqwvfoura  46656  fouriersw  46659  etransclem1  46663  etransclem4  46666  etransclem17  46679  etransclem18  46680  etransclem19  46681  etransclem20  46682  etransclem21  46683  etransclem22  46684  etransclem23  46685  etransclem27  46689  etransclem32  46694  etransclem35  46697  etransclem46  46708  ioorrnopnlem  46732  ovnval2  46973  volicorecl  46974  hoiprodcl  46975  ovnf  46991  hsphoif  47004  hsphoival  47007  hoiprodcl3  47008  volicore  47009  hoidmvcl  47010  hsphoidmvle2  47013  hsphoidmvle  47014  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmvlelem2  47024  hoidmvlelem3  47025  ovnhoilem1  47029  hoidifhspf  47046  hoidifhspval3  47047  ovolval4lem1  47077  ovolval4lem2  47078  smfmullem1  47219  smfmullem2  47220  smfmullem3  47221  afv2ex  47662  suppmptcfin  48852  linc1  48901  lcoss  48912  el0ldep  48942