Theorem ifcld 4514

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

Syntax hints:   → wi 4   ∈ wcel 2114  ifcif 4467

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 4468

This theorem is referenced by:  ifexd  4516  soltmin  6095  pw2f1olem  9014  unxpdomlem3  9163  wemaplem2  9457  cantnfp1lem1  9594  cantnfp1lem2  9595  cantnfp1lem3  9596  cantnflem1d  9604  cantnflem1  9605  ssfzunsnext  13518  tpf  14456  relexpsucnnr  14982  rexuzre  15310  rexico  15311  limsupgre  15438  rlim3  15455  o1lo1  15494  rlimclim1  15502  lo1resb  15521  o1resb  15523  o1of2  15570  o1rlimmul  15576  lo1le  15609  ruclem1  16193  ruclem10  16201  bitsfzo  16399  ramub1lem2  16993  ramcl  16995  prmocl  17000  prmop1  17004  prmdvdsprmo  17008  prmolefac  17012  prmodvdslcmf  17013  prmgapprmo  17028  setsstruct2  17139  wunress  17214  opifismgm  18622  mulgfval  19040  frgpuptf  19740  gsumzsplit  19897  gsummpt1n0  19935  xrsds  21403  uvcvvcl2  21782  uvcff  21785  snifpsrbag  21914  psr1cl  21953  subrgpsr  21970  mvrf  21977  mplmon  22027  mplmonmul  22028  mplcoe1  22029  evlslem3  22072  evlslem1  22074  coe1tmfv2  22254  gsummoncoe1  22287  rhmmpl  22362  rhmply1vr1  22366  mamumat1cl  22418  dmatmulcl  22479  scmatscmiddistr  22487  1mavmul  22527  marrepeval  22542  marrepcl  22543  marepveval  22547  marepvcl  22548  mdetrsca2  22583  mdetr0  22584  mdetrlin2  22586  mdetralt2  22588  mdetero  22589  mdetunilem2  22592  mdetunilem5  22595  mdetunilem6  22596  mdetunilem8  22598  mdetunilem9  22599  maducoeval2  22619  maduf  22620  madutpos  22621  madugsum  22622  gsummatr01lem3  22636  marep01ma  22639  smadiadetglem2  22651  monmatcollpw  22758  pmatcollpw3fi1lem1  22765  pmatcollpw3fi1lem2  22766  xkopt  23634  tsmssplit  24131  ssblex  24407  stdbdxmet  24494  stdbdmet  24495  stdbdbl  24496  stdbdmopn  24497  nlmvscnlem1  24665  tgioo  24775  xrsxmet  24789  icccmplem2  24803  ipcnlem1  25226  ivthlem2  25433  ovolicc2lem5  25502  ioombl1lem1  25539  ioombl1lem3  25541  ioombl1lem4  25542  mbfmax  25630  i1fres  25686  itg1climres  25695  mbfi1fseqlem3  25698  mbfi1fseqlem4  25699  mbfi1fseqlem5  25700  limcres  25867  dvferm1lem  25965  dvferm2lem  25967  dvlip2  25976  lhop1  25995  dvfsumrlim  26012  mdegaddle  26053  deg1addle2  26081  deg1sublt  26089  ply1divmo  26115  plyaddlem1  26192  plyaddlem  26194  coeaddlem  26228  dgradd2  26247  plydiveu  26279  abelthlem9  26422  logcnlem2  26624  logcnlem3  26625  cxpcn3lem  26728  lgamgulmlem4  27013  lgamgulmlem6  27015  ftalem2  27055  gausslemma2dlem4  27350  chebbnd1lem1  27450  dchrisumlem3  27472  dchrvmasumiflem1  27482  ostth3  27619  abssval  28249  absscl  28250  axlowdimlem15  29043  elrspunsn  33508  ply1moneq  33667  deg1addlt  33679  extvfvv  33697  extvfvvcl  33698  extvfvcl  33699  mplvrpmrhm  33710  psrmon  33712  psrmonmul  33713  psrmonprod  33715  mplmonprod  33717  esplyfval0  33727  esplyfval1  33736  esplyind  33738  fldextrspunlsp  33838  dstfrvunirn  34639  circlemeth  34804  indispconn  35436  ex-sategoelel  35623  ex-sategoelelomsuc  35628  knoppndvlem18  36809  itg2addnclem2  38011  itg2addnclem3  38012  ftc1anclem5  38036  sticksstones10  42612  sticksstones12a  42614  aks6d1c6lem3  42629  rhmpsr  43013  evlsbagval  43020  selvvvval  43036  fsuppind  43041  fsuppssind  43044  mhpind  43045  dffltz  43085  irrapxlem4  43275  irrapxlem5  43276  kelac1  43513  areaquad  43666  cantnfresb  43774  sqrtcval  44090  clsk1indlem4  44493  mnringmulrcld  44677  refsum2cnlem1  45490  rexabslelem  45868  uzublem  45880  ioondisj2  45945  ioondisj1  45946  uzubioo  46017  mullimc  46068  mullimcf  46075  lptioo2  46083  limcleqr  46094  0ellimcdiv  46099  limsupubuzlem  46162  limsupequzmptlem  46178  climxrre  46200  limsup10exlem  46222  limsup10ex  46223  liminf10ex  46224  liminflelimsuplem  46225  icccncfext  46337  cncfiooicclem1  46343  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  stoweid  46513  fourierdlem9  46566  fourierdlem10  46567  fourierdlem37  46594  fourierdlem40  46597  fourierdlem66  46622  fourierdlem73  46629  fourierdlem74  46630  fourierdlem75  46631  fourierdlem78  46634  fourierdlem79  46635  fourierdlem95  46651  fourierdlem103  46659  sqwvfoura  46678  fouriersw  46681  etransclem1  46685  etransclem4  46688  etransclem17  46701  etransclem18  46702  etransclem19  46703  etransclem20  46704  etransclem21  46705  etransclem22  46706  etransclem23  46707  etransclem27  46711  etransclem32  46716  etransclem35  46719  etransclem46  46730  ioorrnopnlem  46754  ovnval2  46995  volicorecl  46996  hoiprodcl  46997  ovnf  47013  hsphoif  47026  hsphoival  47029  hoiprodcl3  47030  volicore  47031  hoidmvcl  47032  hsphoidmvle2  47035  hsphoidmvle  47036  hoidmv1lelem1  47041  hoidmv1lelem2  47042  hoidmv1lelem3  47043  hoidmvlelem2  47046  hoidmvlelem3  47047  ovnhoilem1  47051  hoidifhspf  47068  hoidifhspval3  47069  ovolval4lem1  47099  ovolval4lem2  47100  smfmullem1  47241  smfmullem2  47242  smfmullem3  47243  afv2ex  47678  suppmptcfin  48868  linc1  48917  lcoss  48928  el0ldep  48958