Theorem ifcld 4502

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

Syntax hints:   → wi 4   ∈ wcel 2108  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  ifexd  4504  soltmin  6030  pw2f1olem  8816  unxpdomlem3  8958  wemaplem2  9236  cantnfp1lem1  9366  cantnfp1lem2  9367  cantnfp1lem3  9368  cantnflem1d  9376  cantnflem1  9377  ssfzunsnext  13230  relexpsucnnr  14664  rexuzre  14992  rexico  14993  limsupgre  15118  rlim3  15135  o1lo1  15174  rlimclim1  15182  lo1resb  15201  o1resb  15203  o1of2  15250  o1rlimmul  15256  lo1le  15291  ruclem1  15868  ruclem10  15876  bitsfzo  16070  ramub1lem2  16656  ramcl  16658  prmocl  16663  prmop1  16667  prmdvdsprmo  16671  prmolefac  16675  prmodvdslcmf  16676  prmgapprmo  16691  setsstruct2  16803  wunress  16886  wunressOLD  16887  opifismgm  18258  mulgfval  18617  frgpuptf  19291  gsumzsplit  19443  gsummpt1n0  19481  xrsds  20553  uvcvvcl2  20905  uvcff  20908  snifpsrbag  21035  psr1cl  21081  subrgpsr  21098  mvrf  21103  mplmon  21146  mplmonmul  21147  mplcoe1  21148  evlslem3  21200  evlslem1  21202  coe1tmfv2  21356  gsummoncoe1  21385  mamumat1cl  21496  dmatmulcl  21557  scmatscmiddistr  21565  1mavmul  21605  marrepeval  21620  marrepcl  21621  marepveval  21625  marepvcl  21626  mdetrsca2  21661  mdetr0  21662  mdetrlin2  21664  mdetralt2  21666  mdetero  21667  mdetunilem2  21670  mdetunilem5  21673  mdetunilem6  21674  mdetunilem8  21676  mdetunilem9  21677  maducoeval2  21697  maduf  21698  madutpos  21699  madugsum  21700  gsummatr01lem3  21714  marep01ma  21717  smadiadetglem2  21729  monmatcollpw  21836  pmatcollpw3fi1lem1  21843  pmatcollpw3fi1lem2  21844  xkopt  22714  tsmssplit  23211  ssblex  23489  stdbdxmet  23577  stdbdmet  23578  stdbdbl  23579  stdbdmopn  23580  nlmvscnlem1  23756  tgioo  23865  xrsxmet  23878  icccmplem2  23892  ipcnlem1  24314  ivthlem2  24521  ovolicc2lem5  24590  ioombl1lem1  24627  ioombl1lem3  24629  ioombl1lem4  24630  mbfmax  24718  i1fres  24775  itg1climres  24784  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  limcres  24955  dvferm1lem  25053  dvferm2lem  25055  dvlip2  25064  lhop1  25083  dvfsumrlim  25100  mdegaddle  25144  deg1addle2  25172  deg1sublt  25180  ply1divmo  25205  plyaddlem1  25279  plyaddlem  25281  coeaddlem  25315  dgradd2  25334  plydiveu  25363  abelthlem9  25504  logcnlem2  25703  logcnlem3  25704  cxpcn3lem  25805  lgamgulmlem4  26086  lgamgulmlem6  26088  ftalem2  26128  gausslemma2dlem4  26422  chebbnd1lem1  26522  dchrisumlem3  26544  dchrvmasumiflem1  26554  ostth3  26691  axlowdimlem15  27227  dstfrvunirn  32341  circlemeth  32520  indispconn  33096  ex-sategoelel  33283  ex-sategoelelomsuc  33288  knoppndvlem18  34636  itg2addnclem2  35756  itg2addnclem3  35757  ftc1anclem5  35781  sticksstones10  40039  sticksstones12a  40041  metakunt3  40055  metakunt4  40056  metakunt29  40081  metakunt30  40082  metakunt32  40084  metakunt33  40085  evlsbagval  40198  fsuppind  40202  fsuppssind  40205  mhpind  40206  mhphf  40208  dffltz  40387  irrapxlem4  40563  irrapxlem5  40564  kelac1  40804  areaquad  40963  sqrtcval  41138  clsk1indlem4  41543  mnringmulrcld  41735  refsum2cnlem1  42469  rexabslelem  42848  uzublem  42860  ioondisj2  42921  ioondisj1  42922  uzubioo  42995  mullimc  43047  mullimcf  43054  lptioo2  43062  limcleqr  43075  0ellimcdiv  43080  limsupubuzlem  43143  limsupequzmptlem  43159  climxrre  43181  limsup10exlem  43203  limsup10ex  43204  liminf10ex  43205  liminflelimsuplem  43206  icccncfext  43318  cncfiooicclem1  43324  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  stoweid  43494  fourierdlem9  43547  fourierdlem10  43548  fourierdlem37  43575  fourierdlem40  43578  fourierdlem66  43603  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem78  43615  fourierdlem79  43616  fourierdlem95  43632  fourierdlem103  43640  sqwvfoura  43659  fouriersw  43662  etransclem1  43666  etransclem4  43669  etransclem17  43682  etransclem18  43683  etransclem19  43684  etransclem20  43685  etransclem21  43686  etransclem22  43687  etransclem23  43688  etransclem27  43692  etransclem32  43697  etransclem35  43700  etransclem46  43711  ioorrnopnlem  43735  ovnval2  43973  volicorecl  43974  hoiprodcl  43975  ovnf  43991  hsphoif  44004  hsphoival  44007  hoiprodcl3  44008  volicore  44009  hoidmvcl  44010  hsphoidmvle2  44013  hsphoidmvle  44014  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnhoilem1  44029  hoidifhspf  44046  hoidifhspval3  44047  ovolval4lem1  44077  ovolval4lem2  44078  smfmullem1  44212  smfmullem2  44213  smfmullem3  44214  afv2ex  44593  suppmptcfin  45603  linc1  45654  lcoss  45665  el0ldep  45695