Theorem ifcld 4529

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  ifexd  4531  soltmin  6130  pw2f1olem  9100  unxpdomlem3  9249  wemaplem2  9541  cantnfp1lem1  9679  cantnfp1lem2  9680  cantnfp1lem3  9681  cantnflem1d  9689  cantnflem1  9690  ssfzunsnext  13703  tpf  14644  relexpsucnnr  15178  rexuzre  15520  rexico  15521  limsupgre  15648  rlim3  15665  o1lo1  15704  rlimclim1  15712  lo1resb  15731  o1resb  15733  o1of2  15780  o1rlimmul  15786  lo1le  15819  ruclem1  16399  ruclem10  16407  bitsfzo  16605  ramub1lem2  17205  ramcl  17207  prmocl  17212  prmop1  17216  prmdvdsprmo  17220  prmolefac  17224  prmodvdslcmf  17225  prmgapprmo  17240  setsstruct2  17352  wunress  17427  opifismgm  18837  mulgfval  19279  frgpuptf  19984  gsumzsplit  20141  gsummpt1n0  20179  xrsds  21716  uvcvvcl2  22094  uvcff  22097  snifpsrbag  22228  psr1cl  22268  subrgpsr  22285  mvrf  22292  mplmon  22344  mplmonmul  22345  mplcoe1  22346  evlslem3  22389  evlslem1  22391  selvvvval  22451  coe1tmfv2  22594  gsummoncoe1  22626  rhmmpl  22698  rhmply1vr1  22702  mamumat1cl  22754  dmatmulcl  22815  scmatscmiddistr  22823  1mavmul  22863  marrepeval  22878  marrepcl  22879  marepveval  22883  marepvcl  22884  mdetrsca2  22919  mdetr0  22920  mdetrlin2  22922  mdetralt2  22924  mdetero  22925  mdetunilem2  22928  mdetunilem5  22931  mdetunilem6  22932  mdetunilem8  22934  mdetunilem9  22935  maducoeval2  22955  maduf  22956  madutpos  22957  madugsum  22958  gsummatr01lem3  22972  marep01ma  22975  smadiadetglem2  22987  monmatcollpw  23097  pmatcollpw3fi1lem1  23104  pmatcollpw3fi1lem2  23105  xkopt  23974  tsmssplit  24471  ssblex  24747  stdbdxmet  24834  stdbdmet  24835  stdbdbl  24836  stdbdmopn  24837  nlmvscnlem1  25005  tgioo  25115  xrsxmet  25129  icccmplem2  25143  ipcnlem1  25566  ivthlem2  25773  ovolicc2lem5  25842  ioombl1lem1  25879  ioombl1lem3  25881  ioombl1lem4  25882  mbfmax  25970  i1fres  26026  itg1climres  26035  mbfi1fseqlem3  26038  mbfi1fseqlem4  26039  mbfi1fseqlem5  26040  limcres  26206  dvferm1lem  26304  dvferm2lem  26306  dvlip2  26315  lhop1  26334  dvfsumrlim  26351  mdegaddle  26392  deg1addle2  26420  deg1sublt  26428  ply1divmo  26454  plyaddlem1  26532  plyaddlem  26534  coeaddlem  26568  dgradd2  26587  plydiveu  26619  abelthlem9  26767  logcnlem2  26971  logcnlem3  26972  cxpcn3lem  27075  lgamgulmlem4  27359  lgamgulmlem6  27361  ftalem2  27401  gausslemma2dlem4  27696  chebbnd1lem1  27796  dchrisumlem3  27818  dchrvmasumiflem1  27828  ostth3  27965  abssval  28625  absscl  28626  axlowdimlem15  29534  elrspunsn  33979  ply1moneq  34120  deg1addlt  34132  mplasclco  34148  selvply1rhmlem2  34153  extvfvv  34166  extvfvvcl  34167  extvfvcl  34168  mplvrpmrhm  34179  psrmon  34181  psrmonmul  34182  psrmonprod  34184  mplmonprod  34186  esplyfval0  34196  esplyfval1  34205  esplyind  34207  fldextrspunlsp  34306  dstfrvunirn  35107  circlemeth  35269  indispconn  35999  ex-sategoelel  36186  ex-sategoelelomsuc  36191  knoppndvlem18  37395  itg2addnclem2  38590  itg2addnclem3  38591  ftc1anclem5  38615  sticksstones10  43205  sticksstones12a  43207  aks6d1c6lem3  43222  rhmpsr  43611  evlsbagval  43614  fsuppind  43618  fsuppssind  43621  mhpind  43622  dffltz  43670  irrapxlem4  43831  irrapxlem5  43832  kelac1  44064  areaquad  44217  cantnfresb  44325  sqrtcval  44640  clsk1indlem4  45043  mnringmulrcld  45225  refsum2cnlem1  46053  rexabslelem  46427  uzublem  46439  ioondisj2  46504  ioondisj1  46505  uzubioo  46576  mullimc  46627  mullimcf  46634  lptioo2  46642  limcleqr  46653  0ellimcdiv  46658  limsupubuzlem  46721  limsupequzmptlem  46737  climxrre  46759  limsup10exlem  46781  limsup10ex  46782  liminf10ex  46783  liminflelimsuplem  46784  icccncfext  46896  cncfiooicclem1  46902  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  stoweid  47072  fourierdlem9  47125  fourierdlem10  47126  fourierdlem37  47153  fourierdlem40  47156  fourierdlem66  47181  fourierdlem73  47188  fourierdlem74  47189  fourierdlem75  47190  fourierdlem78  47193  fourierdlem79  47194  fourierdlem95  47210  fourierdlem103  47218  sqwvfoura  47237  fouriersw  47240  etransclem1  47244  etransclem4  47247  etransclem17  47260  etransclem18  47261  etransclem19  47262  etransclem20  47263  etransclem21  47264  etransclem22  47265  etransclem23  47266  etransclem27  47270  etransclem32  47275  etransclem35  47278  etransclem46  47289  ioorrnopnlem  47313  ovnval2  47554  volicorecl  47555  hoiprodcl  47556  ovnf  47572  hsphoif  47585  hsphoival  47588  hoiprodcl3  47589  volicore  47590  hoidmvcl  47591  hsphoidmvle2  47594  hsphoidmvle  47595  hoidmv1lelem1  47600  hoidmv1lelem2  47601  hoidmv1lelem3  47602  hoidmvlelem2  47605  hoidmvlelem3  47606  ovnhoilem1  47610  hoidifhspf  47627  hoidifhspval3  47628  ovolval4lem1  47658  ovolval4lem2  47659  smfmullem1  47800  smfmullem2  47801  smfmullem3  47802  tmachlem-agreeprod  47946  tmachlem-tpopen  47950  afv2ex  48283  suppmptcfin  49487  linc1  49536  lcoss  49547  el0ldep  49577  crosspclem  50957  veronesefvcl  50971