Theorem ifcld 4470

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

Syntax hints:   → wi 4   ∈ wcel 2114  ifcif 4424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-if 4425

This theorem is referenced by:  ifexd  4472  soltmin  5980  pw2f1olem  8683  unxpdomlem3  8816  wemaplem2  9097  cantnfp1lem1  9227  cantnfp1lem2  9228  cantnfp1lem3  9229  cantnflem1d  9237  cantnflem1  9238  ssfzunsnext  13056  relexpsucnnr  14487  rexuzre  14815  rexico  14816  limsupgre  14941  rlim3  14958  o1lo1  14997  rlimclim1  15005  lo1resb  15024  o1resb  15026  o1of2  15073  o1rlimmul  15079  lo1le  15114  ruclem1  15689  ruclem10  15697  bitsfzo  15891  ramub1lem2  16476  ramcl  16478  prmocl  16483  prmop1  16487  prmdvdsprmo  16491  prmolefac  16495  prmodvdslcmf  16496  prmgapprmo  16511  setsstruct2  16637  wunress  16680  opifismgm  17998  mulgfval  18357  frgpuptf  19027  gsumzsplit  19179  gsummpt1n0  19217  xrsds  20273  uvcvvcl2  20617  uvcff  20620  snifpsrbag  20748  psr1cl  20794  subrgpsr  20811  mvrf  20816  mplmon  20859  mplmonmul  20860  mplcoe1  20861  evlslem3  20907  evlslem1  20909  coe1tmfv2  21063  gsummoncoe1  21092  mamumat1cl  21203  dmatmulcl  21264  scmatscmiddistr  21272  1mavmul  21312  marrepeval  21327  marrepcl  21328  marepveval  21332  marepvcl  21333  mdetrsca2  21368  mdetr0  21369  mdetrlin2  21371  mdetralt2  21373  mdetero  21374  mdetunilem2  21377  mdetunilem5  21380  mdetunilem6  21381  mdetunilem8  21383  mdetunilem9  21384  maducoeval2  21404  maduf  21405  madutpos  21406  madugsum  21407  gsummatr01lem3  21421  marep01ma  21424  smadiadetglem2  21436  monmatcollpw  21543  pmatcollpw3fi1lem1  21550  pmatcollpw3fi1lem2  21551  xkopt  22419  tsmssplit  22916  ssblex  23194  stdbdxmet  23281  stdbdmet  23282  stdbdbl  23283  stdbdmopn  23284  nlmvscnlem1  23452  tgioo  23561  xrsxmet  23574  icccmplem2  23588  ipcnlem1  24010  ivthlem2  24217  ovolicc2lem5  24286  ioombl1lem1  24323  ioombl1lem3  24325  ioombl1lem4  24326  mbfmax  24414  i1fres  24471  itg1climres  24480  mbfi1fseqlem3  24483  mbfi1fseqlem4  24484  mbfi1fseqlem5  24485  limcres  24651  dvferm1lem  24749  dvferm2lem  24751  dvlip2  24760  lhop1  24779  dvfsumrlim  24796  mdegaddle  24840  deg1addle2  24868  deg1sublt  24876  ply1divmo  24901  plyaddlem1  24975  plyaddlem  24977  coeaddlem  25011  dgradd2  25030  plydiveu  25059  abelthlem9  25200  logcnlem2  25399  logcnlem3  25400  cxpcn3lem  25501  lgamgulmlem4  25782  lgamgulmlem6  25784  ftalem2  25824  gausslemma2dlem4  26118  chebbnd1lem1  26218  dchrisumlem3  26240  dchrvmasumiflem1  26250  ostth3  26387  axlowdimlem15  26915  dstfrvunirn  32024  circlemeth  32203  indispconn  32780  ex-sategoelel  32967  ex-sategoelelomsuc  32972  knoppndvlem18  34365  itg2addnclem2  35485  itg2addnclem3  35486  ftc1anclem5  35510  sticksstones10  39750  sticksstones12a  39752  metakunt3  39759  metakunt4  39760  metakunt29  39785  metakunt30  39786  metakunt32  39788  metakunt33  39789  evlsbagval  39895  fsuppind  39899  fsuppssind  39902  mhpind  39903  mhphf  39905  dffltz  40084  irrapxlem4  40260  irrapxlem5  40261  kelac1  40501  areaquad  40660  sqrtcval  40835  clsk1indlem4  41241  mnringmulrcld  41429  refsum2cnlem1  42159  rexabslelem  42537  uzublem  42549  ioondisj2  42612  ioondisj1  42613  uzubioo  42686  mullimc  42740  mullimcf  42747  lptioo2  42755  limcleqr  42768  0ellimcdiv  42773  limsupubuzlem  42836  limsupequzmptlem  42852  climxrre  42874  limsup10exlem  42896  limsup10ex  42897  liminf10ex  42898  liminflelimsuplem  42899  icccncfext  43011  cncfiooicclem1  43017  ioodvbdlimc1lem2  43056  ioodvbdlimc2lem  43058  stoweid  43187  fourierdlem9  43240  fourierdlem10  43241  fourierdlem37  43268  fourierdlem40  43271  fourierdlem66  43296  fourierdlem73  43303  fourierdlem74  43304  fourierdlem75  43305  fourierdlem78  43308  fourierdlem79  43309  fourierdlem95  43325  fourierdlem103  43333  sqwvfoura  43352  fouriersw  43355  etransclem1  43359  etransclem4  43362  etransclem17  43375  etransclem18  43376  etransclem19  43377  etransclem20  43378  etransclem21  43379  etransclem22  43380  etransclem23  43381  etransclem27  43385  etransclem32  43390  etransclem35  43393  etransclem46  43404  ioorrnopnlem  43428  ovnval2  43666  volicorecl  43667  hoiprodcl  43668  ovnf  43684  hsphoif  43697  hsphoival  43700  hoiprodcl3  43701  volicore  43702  hoidmvcl  43703  hsphoidmvle2  43706  hsphoidmvle  43707  hoidmv1lelem1  43712  hoidmv1lelem2  43713  hoidmv1lelem3  43714  hoidmvlelem2  43717  hoidmvlelem3  43718  ovnhoilem1  43722  hoidifhspf  43739  hoidifhspval3  43740  ovolval4lem1  43770  ovolval4lem2  43771  smfmullem1  43905  smfmullem2  43906  smfmullem3  43907  afv2ex  44287  suppmptcfin  45297  linc1  45348  lcoss  45359  el0ldep  45389