Theorem ifcld 4539

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

Syntax hints:   → wi 4   ∈ wcel 2149  ifcif 4492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-if 4493

This theorem is referenced by:  ifexd  4541  soltmin  6137  pw2f1olem  9069  unxpdomlem3  9218  wemaplem2  9509  cantnfp1lem1  9647  cantnfp1lem2  9648  cantnfp1lem3  9649  cantnflem1d  9657  cantnflem1  9658  ssfzunsnext  13597  tpf  14536  relexpsucnnr  15062  rexuzre  15404  rexico  15405  limsupgre  15532  rlim3  15549  o1lo1  15588  rlimclim1  15596  lo1resb  15615  o1resb  15617  o1of2  15664  o1rlimmul  15670  lo1le  15703  ruclem1  16287  ruclem10  16295  bitsfzo  16493  ramub1lem2  17087  ramcl  17089  prmocl  17094  prmop1  17098  prmdvdsprmo  17102  prmolefac  17106  prmodvdslcmf  17107  prmgapprmo  17122  setsstruct2  17234  wunress  17309  opifismgm  18717  mulgfval  19135  frgpuptf  19840  gsumzsplit  19997  gsummpt1n0  20035  xrsds  21529  uvcvvcl2  21907  uvcff  21910  snifpsrbag  22039  psr1cl  22079  subrgpsr  22096  mvrf  22103  mplmon  22155  mplmonmul  22156  mplcoe1  22157  evlslem3  22200  evlslem1  22202  selvvvval  22262  coe1tmfv2  22405  gsummoncoe1  22437  rhmmpl  22509  rhmply1vr1  22513  mamumat1cl  22565  dmatmulcl  22626  scmatscmiddistr  22634  1mavmul  22674  marrepeval  22689  marrepcl  22690  marepveval  22694  marepvcl  22695  mdetrsca2  22730  mdetr0  22731  mdetrlin2  22733  mdetralt2  22735  mdetero  22736  mdetunilem2  22739  mdetunilem5  22742  mdetunilem6  22743  mdetunilem8  22745  mdetunilem9  22746  maducoeval2  22766  maduf  22767  madutpos  22768  madugsum  22769  gsummatr01lem3  22783  marep01ma  22786  smadiadetglem2  22798  monmatcollpw  22905  pmatcollpw3fi1lem1  22912  pmatcollpw3fi1lem2  22913  xkopt  23781  tsmssplit  24278  ssblex  24554  stdbdxmet  24641  stdbdmet  24642  stdbdbl  24643  stdbdmopn  24644  nlmvscnlem1  24812  tgioo  24922  xrsxmet  24936  icccmplem2  24950  ipcnlem1  25373  ivthlem2  25580  ovolicc2lem5  25649  ioombl1lem1  25686  ioombl1lem3  25688  ioombl1lem4  25689  mbfmax  25777  i1fres  25833  itg1climres  25842  mbfi1fseqlem3  25845  mbfi1fseqlem4  25846  mbfi1fseqlem5  25847  limcres  26014  dvferm1lem  26112  dvferm2lem  26114  dvlip2  26123  lhop1  26142  dvfsumrlim  26159  mdegaddle  26200  deg1addle2  26228  deg1sublt  26236  ply1divmo  26262  plyaddlem1  26339  plyaddlem  26341  coeaddlem  26375  dgradd2  26394  plydiveu  26428  abelthlem9  26569  logcnlem2  26774  logcnlem3  26775  cxpcn3lem  26878  lgamgulmlem4  27162  lgamgulmlem6  27164  ftalem2  27204  gausslemma2dlem4  27499  chebbnd1lem1  27599  dchrisumlem3  27621  dchrvmasumiflem1  27631  ostth3  27768  abssval  28398  absscl  28399  axlowdimlem15  29247  elrspunsn  33681  ply1moneq  33823  deg1addlt  33835  mplasclco  33851  selvply1rhmlem2  33856  extvfvv  33869  extvfvvcl  33870  extvfvcl  33871  mplvrpmrhm  33882  psrmon  33884  psrmonmul  33885  psrmonprod  33887  mplmonprod  33889  esplyfval0  33899  esplyfval1  33908  esplyind  33910  fldextrspunlsp  34009  dstfrvunirn  34810  circlemeth  34972  indispconn  35659  ex-sategoelel  35846  ex-sategoelelomsuc  35851  knoppndvlem18  37041  itg2addnclem2  38245  itg2addnclem3  38246  ftc1anclem5  38270  sticksstones10  42846  sticksstones12a  42848  aks6d1c6lem3  42863  rhmpsr  43241  evlsbagval  43244  fsuppind  43248  fsuppssind  43251  mhpind  43252  dffltz  43292  irrapxlem4  43478  irrapxlem5  43479  kelac1  43716  areaquad  43869  cantnfresb  43977  sqrtcval  44293  clsk1indlem4  44696  mnringmulrcld  44878  refsum2cnlem1  45683  rexabslelem  46058  uzublem  46070  ioondisj2  46135  ioondisj1  46136  uzubioo  46207  mullimc  46258  mullimcf  46265  lptioo2  46273  limcleqr  46284  0ellimcdiv  46289  limsupubuzlem  46352  limsupequzmptlem  46368  climxrre  46390  limsup10exlem  46412  limsup10ex  46413  liminf10ex  46414  liminflelimsuplem  46415  icccncfext  46527  cncfiooicclem1  46533  ioodvbdlimc1lem2  46572  ioodvbdlimc2lem  46574  stoweid  46703  fourierdlem9  46756  fourierdlem10  46757  fourierdlem37  46784  fourierdlem40  46787  fourierdlem66  46812  fourierdlem73  46819  fourierdlem74  46820  fourierdlem75  46821  fourierdlem78  46824  fourierdlem79  46825  fourierdlem95  46841  fourierdlem103  46849  sqwvfoura  46868  fouriersw  46871  etransclem1  46875  etransclem4  46878  etransclem17  46891  etransclem18  46892  etransclem19  46893  etransclem20  46894  etransclem21  46895  etransclem22  46896  etransclem23  46897  etransclem27  46901  etransclem32  46906  etransclem35  46909  etransclem46  46920  ioorrnopnlem  46944  ovnval2  47185  volicorecl  47186  hoiprodcl  47187  ovnf  47203  hsphoif  47216  hsphoival  47219  hoiprodcl3  47220  volicore  47221  hoidmvcl  47222  hsphoidmvle2  47225  hsphoidmvle  47226  hoidmv1lelem1  47231  hoidmv1lelem2  47232  hoidmv1lelem3  47233  hoidmvlelem2  47236  hoidmvlelem3  47237  ovnhoilem1  47241  hoidifhspf  47258  hoidifhspval3  47259  ovolval4lem1  47289  ovolval4lem2  47290  smfmullem1  47431  smfmullem2  47432  smfmullem3  47433  afv2ex  47874  suppmptcfin  49075  linc1  49124  lcoss  49135  el0ldep  49165