Theorem ifcld 4528

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

Syntax hints:   → wi 4   ∈ wcel 2114  ifcif 4481

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 4482

This theorem is referenced by:  ifexd  4530  soltmin  6103  pw2f1olem  9023  unxpdomlem3  9172  wemaplem2  9466  cantnfp1lem1  9601  cantnfp1lem2  9602  cantnfp1lem3  9603  cantnflem1d  9611  cantnflem1  9612  ssfzunsnext  13499  tpf  14436  relexpsucnnr  14962  rexuzre  15290  rexico  15291  limsupgre  15418  rlim3  15435  o1lo1  15474  rlimclim1  15482  lo1resb  15501  o1resb  15503  o1of2  15550  o1rlimmul  15556  lo1le  15589  ruclem1  16170  ruclem10  16178  bitsfzo  16376  ramub1lem2  16969  ramcl  16971  prmocl  16976  prmop1  16980  prmdvdsprmo  16984  prmolefac  16988  prmodvdslcmf  16989  prmgapprmo  17004  setsstruct2  17115  wunress  17190  opifismgm  18598  mulgfval  19016  frgpuptf  19716  gsumzsplit  19873  gsummpt1n0  19911  xrsds  21381  uvcvvcl2  21760  uvcff  21763  snifpsrbag  21893  psr1cl  21933  subrgpsr  21950  mvrf  21957  mplmon  22007  mplmonmul  22008  mplcoe1  22009  evlslem3  22052  evlslem1  22054  coe1tmfv2  22234  gsummoncoe1  22269  rhmmpl  22344  rhmply1vr1  22348  mamumat1cl  22400  dmatmulcl  22461  scmatscmiddistr  22469  1mavmul  22509  marrepeval  22524  marrepcl  22525  marepveval  22529  marepvcl  22530  mdetrsca2  22565  mdetr0  22566  mdetrlin2  22568  mdetralt2  22570  mdetero  22571  mdetunilem2  22574  mdetunilem5  22577  mdetunilem6  22578  mdetunilem8  22580  mdetunilem9  22581  maducoeval2  22601  maduf  22602  madutpos  22603  madugsum  22604  gsummatr01lem3  22618  marep01ma  22621  smadiadetglem2  22633  monmatcollpw  22740  pmatcollpw3fi1lem1  22747  pmatcollpw3fi1lem2  22748  xkopt  23616  tsmssplit  24113  ssblex  24389  stdbdxmet  24476  stdbdmet  24477  stdbdbl  24478  stdbdmopn  24479  nlmvscnlem1  24647  tgioo  24757  xrsxmet  24771  icccmplem2  24785  ipcnlem1  25218  ivthlem2  25426  ovolicc2lem5  25495  ioombl1lem1  25532  ioombl1lem3  25534  ioombl1lem4  25535  mbfmax  25623  i1fres  25679  itg1climres  25688  mbfi1fseqlem3  25691  mbfi1fseqlem4  25692  mbfi1fseqlem5  25693  limcres  25860  dvferm1lem  25961  dvferm2lem  25963  dvlip2  25973  lhop1  25992  dvfsumrlim  26011  mdegaddle  26052  deg1addle2  26080  deg1sublt  26088  ply1divmo  26114  plyaddlem1  26191  plyaddlem  26193  coeaddlem  26227  dgradd2  26247  plydiveu  26279  abelthlem9  26423  logcnlem2  26625  logcnlem3  26626  cxpcn3lem  26730  lgamgulmlem4  27015  lgamgulmlem6  27017  ftalem2  27057  gausslemma2dlem4  27353  chebbnd1lem1  27453  dchrisumlem3  27475  dchrvmasumiflem1  27485  ostth3  27622  abssval  28252  absscl  28253  axlowdimlem15  29047  elrspunsn  33528  ply1moneq  33687  deg1addlt  33699  extvfvv  33717  extvfvvcl  33718  extvfvcl  33719  mplvrpmrhm  33730  psrmon  33732  psrmonmul  33733  psrmonprod  33735  mplmonprod  33737  esplyfval0  33747  esplyfval1  33756  esplyind  33758  fldextrspunlsp  33858  dstfrvunirn  34659  circlemeth  34824  indispconn  35456  ex-sategoelel  35643  ex-sategoelelomsuc  35648  knoppndvlem18  36757  itg2addnclem2  37952  itg2addnclem3  37953  ftc1anclem5  37977  sticksstones10  42554  sticksstones12a  42556  aks6d1c6lem3  42571  rhmpsr  42949  evlsbagval  42956  selvvvval  42972  fsuppind  42977  fsuppssind  42980  mhpind  42981  dffltz  43021  irrapxlem4  43211  irrapxlem5  43212  kelac1  43449  areaquad  43602  cantnfresb  43710  sqrtcval  44026  clsk1indlem4  44429  mnringmulrcld  44613  refsum2cnlem1  45426  rexabslelem  45805  uzublem  45817  ioondisj2  45882  ioondisj1  45883  uzubioo  45954  mullimc  46005  mullimcf  46012  lptioo2  46020  limcleqr  46031  0ellimcdiv  46036  limsupubuzlem  46099  limsupequzmptlem  46115  climxrre  46137  limsup10exlem  46159  limsup10ex  46160  liminf10ex  46161  liminflelimsuplem  46162  icccncfext  46274  cncfiooicclem1  46280  ioodvbdlimc1lem2  46319  ioodvbdlimc2lem  46321  stoweid  46450  fourierdlem9  46503  fourierdlem10  46504  fourierdlem37  46531  fourierdlem40  46534  fourierdlem66  46559  fourierdlem73  46566  fourierdlem74  46567  fourierdlem75  46568  fourierdlem78  46571  fourierdlem79  46572  fourierdlem95  46588  fourierdlem103  46596  sqwvfoura  46615  fouriersw  46618  etransclem1  46622  etransclem4  46625  etransclem17  46638  etransclem18  46639  etransclem19  46640  etransclem20  46641  etransclem21  46642  etransclem22  46643  etransclem23  46644  etransclem27  46648  etransclem32  46653  etransclem35  46656  etransclem46  46667  ioorrnopnlem  46691  ovnval2  46932  volicorecl  46933  hoiprodcl  46934  ovnf  46950  hsphoif  46963  hsphoival  46966  hoiprodcl3  46967  volicore  46968  hoidmvcl  46969  hsphoidmvle2  46972  hsphoidmvle  46973  hoidmv1lelem1  46978  hoidmv1lelem2  46979  hoidmv1lelem3  46980  hoidmvlelem2  46983  hoidmvlelem3  46984  ovnhoilem1  46988  hoidifhspf  47005  hoidifhspval3  47006  ovolval4lem1  47036  ovolval4lem2  47037  smfmullem1  47178  smfmullem2  47179  smfmullem3  47180  afv2ex  47603  suppmptcfin  48765  linc1  48814  lcoss  48825  el0ldep  48855