Theorem ifcld 4594

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

Syntax hints:   → wi 4   ∈ wcel 2108  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  ifexd  4596  soltmin  6168  pw2f1olem  9142  unxpdomlem3  9315  wemaplem2  9616  cantnfp1lem1  9747  cantnfp1lem2  9748  cantnfp1lem3  9749  cantnflem1d  9757  cantnflem1  9758  ssfzunsnext  13629  tpf  14548  relexpsucnnr  15074  rexuzre  15401  rexico  15402  limsupgre  15527  rlim3  15544  o1lo1  15583  rlimclim1  15591  lo1resb  15610  o1resb  15612  o1of2  15659  o1rlimmul  15665  lo1le  15700  ruclem1  16279  ruclem10  16287  bitsfzo  16481  ramub1lem2  17074  ramcl  17076  prmocl  17081  prmop1  17085  prmdvdsprmo  17089  prmolefac  17093  prmodvdslcmf  17094  prmgapprmo  17109  setsstruct2  17221  wunress  17309  wunressOLD  17310  opifismgm  18697  mulgfval  19109  frgpuptf  19812  gsumzsplit  19969  gsummpt1n0  20007  xrsds  21450  uvcvvcl2  21831  uvcff  21834  snifpsrbag  21963  psr1cl  22004  subrgpsr  22021  mvrf  22028  mplmon  22076  mplmonmul  22077  mplcoe1  22078  evlslem3  22127  evlslem1  22129  coe1tmfv2  22299  gsummoncoe1  22333  rhmmpl  22408  rhmply1vr1  22412  mamumat1cl  22466  dmatmulcl  22527  scmatscmiddistr  22535  1mavmul  22575  marrepeval  22590  marrepcl  22591  marepveval  22595  marepvcl  22596  mdetrsca2  22631  mdetr0  22632  mdetrlin2  22634  mdetralt2  22636  mdetero  22637  mdetunilem2  22640  mdetunilem5  22643  mdetunilem6  22644  mdetunilem8  22646  mdetunilem9  22647  maducoeval2  22667  maduf  22668  madutpos  22669  madugsum  22670  gsummatr01lem3  22684  marep01ma  22687  smadiadetglem2  22699  monmatcollpw  22806  pmatcollpw3fi1lem1  22813  pmatcollpw3fi1lem2  22814  xkopt  23684  tsmssplit  24181  ssblex  24459  stdbdxmet  24549  stdbdmet  24550  stdbdbl  24551  stdbdmopn  24552  nlmvscnlem1  24728  tgioo  24837  xrsxmet  24850  icccmplem2  24864  ipcnlem1  25298  ivthlem2  25506  ovolicc2lem5  25575  ioombl1lem1  25612  ioombl1lem3  25614  ioombl1lem4  25615  mbfmax  25703  i1fres  25760  itg1climres  25769  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  limcres  25941  dvferm1lem  26042  dvferm2lem  26044  dvlip2  26054  lhop1  26073  dvfsumrlim  26092  mdegaddle  26133  deg1addle2  26161  deg1sublt  26169  ply1divmo  26195  plyaddlem1  26272  plyaddlem  26274  coeaddlem  26308  dgradd2  26328  plydiveu  26358  abelthlem9  26502  logcnlem2  26703  logcnlem3  26704  cxpcn3lem  26808  lgamgulmlem4  27093  lgamgulmlem6  27095  ftalem2  27135  gausslemma2dlem4  27431  chebbnd1lem1  27531  dchrisumlem3  27553  dchrvmasumiflem1  27563  ostth3  27700  abssval  28281  absscl  28282  axlowdimlem15  28989  elrspunsn  33422  ply1moneq  33576  deg1addlt  33585  dstfrvunirn  34439  circlemeth  34617  indispconn  35202  ex-sategoelel  35389  ex-sategoelelomsuc  35394  knoppndvlem18  36495  itg2addnclem2  37632  itg2addnclem3  37633  ftc1anclem5  37657  sticksstones10  42112  sticksstones12a  42114  aks6d1c6lem3  42129  metakunt3  42164  metakunt4  42165  metakunt29  42190  metakunt30  42191  metakunt32  42193  metakunt33  42194  rhmpsr  42507  evlsbagval  42521  selvvvval  42540  fsuppind  42545  fsuppssind  42548  mhpind  42549  dffltz  42589  irrapxlem4  42781  irrapxlem5  42782  kelac1  43020  areaquad  43177  cantnfresb  43286  sqrtcval  43603  clsk1indlem4  44006  mnringmulrcld  44197  refsum2cnlem1  44937  rexabslelem  45333  uzublem  45345  ioondisj2  45411  ioondisj1  45412  uzubioo  45485  mullimc  45537  mullimcf  45544  lptioo2  45552  limcleqr  45565  0ellimcdiv  45570  limsupubuzlem  45633  limsupequzmptlem  45649  climxrre  45671  limsup10exlem  45693  limsup10ex  45694  liminf10ex  45695  liminflelimsuplem  45696  icccncfext  45808  cncfiooicclem1  45814  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  stoweid  45984  fourierdlem9  46037  fourierdlem10  46038  fourierdlem37  46065  fourierdlem40  46068  fourierdlem66  46093  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem78  46105  fourierdlem79  46106  fourierdlem95  46122  fourierdlem103  46130  sqwvfoura  46149  fouriersw  46152  etransclem1  46156  etransclem4  46159  etransclem17  46172  etransclem18  46173  etransclem19  46174  etransclem20  46175  etransclem21  46176  etransclem22  46177  etransclem23  46178  etransclem27  46182  etransclem32  46187  etransclem35  46190  etransclem46  46201  ioorrnopnlem  46225  ovnval2  46466  volicorecl  46467  hoiprodcl  46468  ovnf  46484  hsphoif  46497  hsphoival  46500  hoiprodcl3  46501  volicore  46502  hoidmvcl  46503  hsphoidmvle2  46506  hsphoidmvle  46507  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmvlelem2  46517  hoidmvlelem3  46518  ovnhoilem1  46522  hoidifhspf  46539  hoidifhspval3  46540  ovolval4lem1  46570  ovolval4lem2  46571  smfmullem1  46712  smfmullem2  46713  smfmullem3  46714  afv2ex  47129  suppmptcfin  48104  linc1  48154  lcoss  48165  el0ldep  48195