Theorem ifcld 4538

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

Syntax hints:   → wi 4   ∈ wcel 2109  ifcif 4491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  ifexd  4540  soltmin  6112  pw2f1olem  9050  unxpdomlem3  9206  wemaplem2  9507  cantnfp1lem1  9638  cantnfp1lem2  9639  cantnfp1lem3  9640  cantnflem1d  9648  cantnflem1  9649  ssfzunsnext  13537  tpf  14471  relexpsucnnr  14998  rexuzre  15326  rexico  15327  limsupgre  15454  rlim3  15471  o1lo1  15510  rlimclim1  15518  lo1resb  15537  o1resb  15539  o1of2  15586  o1rlimmul  15592  lo1le  15625  ruclem1  16206  ruclem10  16214  bitsfzo  16412  ramub1lem2  17005  ramcl  17007  prmocl  17012  prmop1  17016  prmdvdsprmo  17020  prmolefac  17024  prmodvdslcmf  17025  prmgapprmo  17040  setsstruct2  17151  wunress  17226  opifismgm  18593  mulgfval  19008  frgpuptf  19707  gsumzsplit  19864  gsummpt1n0  19902  xrsds  21333  uvcvvcl2  21704  uvcff  21707  snifpsrbag  21836  psr1cl  21877  subrgpsr  21894  mvrf  21901  mplmon  21949  mplmonmul  21950  mplcoe1  21951  evlslem3  21994  evlslem1  21996  coe1tmfv2  22168  gsummoncoe1  22202  rhmmpl  22277  rhmply1vr1  22281  mamumat1cl  22333  dmatmulcl  22394  scmatscmiddistr  22402  1mavmul  22442  marrepeval  22457  marrepcl  22458  marepveval  22462  marepvcl  22463  mdetrsca2  22498  mdetr0  22499  mdetrlin2  22501  mdetralt2  22503  mdetero  22504  mdetunilem2  22507  mdetunilem5  22510  mdetunilem6  22511  mdetunilem8  22513  mdetunilem9  22514  maducoeval2  22534  maduf  22535  madutpos  22536  madugsum  22537  gsummatr01lem3  22551  marep01ma  22554  smadiadetglem2  22566  monmatcollpw  22673  pmatcollpw3fi1lem1  22680  pmatcollpw3fi1lem2  22681  xkopt  23549  tsmssplit  24046  ssblex  24323  stdbdxmet  24410  stdbdmet  24411  stdbdbl  24412  stdbdmopn  24413  nlmvscnlem1  24581  tgioo  24691  xrsxmet  24705  icccmplem2  24719  ipcnlem1  25152  ivthlem2  25360  ovolicc2lem5  25429  ioombl1lem1  25466  ioombl1lem3  25468  ioombl1lem4  25469  mbfmax  25557  i1fres  25613  itg1climres  25622  mbfi1fseqlem3  25625  mbfi1fseqlem4  25626  mbfi1fseqlem5  25627  limcres  25794  dvferm1lem  25895  dvferm2lem  25897  dvlip2  25907  lhop1  25926  dvfsumrlim  25945  mdegaddle  25986  deg1addle2  26014  deg1sublt  26022  ply1divmo  26048  plyaddlem1  26125  plyaddlem  26127  coeaddlem  26161  dgradd2  26181  plydiveu  26213  abelthlem9  26357  logcnlem2  26559  logcnlem3  26560  cxpcn3lem  26664  lgamgulmlem4  26949  lgamgulmlem6  26951  ftalem2  26991  gausslemma2dlem4  27287  chebbnd1lem1  27387  dchrisumlem3  27409  dchrvmasumiflem1  27419  ostth3  27556  abssval  28148  absscl  28149  axlowdimlem15  28890  elrspunsn  33407  ply1moneq  33562  deg1addlt  33572  fldextrspunlsp  33676  dstfrvunirn  34473  circlemeth  34638  indispconn  35228  ex-sategoelel  35415  ex-sategoelelomsuc  35420  knoppndvlem18  36524  itg2addnclem2  37673  itg2addnclem3  37674  ftc1anclem5  37698  sticksstones10  42150  sticksstones12a  42152  aks6d1c6lem3  42167  rhmpsr  42547  evlsbagval  42561  selvvvval  42580  fsuppind  42585  fsuppssind  42588  mhpind  42589  dffltz  42629  irrapxlem4  42820  irrapxlem5  42821  kelac1  43059  areaquad  43212  cantnfresb  43320  sqrtcval  43637  clsk1indlem4  44040  mnringmulrcld  44224  refsum2cnlem1  45038  rexabslelem  45421  uzublem  45433  ioondisj2  45498  ioondisj1  45499  uzubioo  45570  mullimc  45621  mullimcf  45628  lptioo2  45636  limcleqr  45649  0ellimcdiv  45654  limsupubuzlem  45717  limsupequzmptlem  45733  climxrre  45755  limsup10exlem  45777  limsup10ex  45778  liminf10ex  45779  liminflelimsuplem  45780  icccncfext  45892  cncfiooicclem1  45898  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweid  46068  fourierdlem9  46121  fourierdlem10  46122  fourierdlem37  46149  fourierdlem40  46152  fourierdlem66  46177  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem78  46189  fourierdlem79  46190  fourierdlem95  46206  fourierdlem103  46214  sqwvfoura  46233  fouriersw  46236  etransclem1  46240  etransclem4  46243  etransclem17  46256  etransclem18  46257  etransclem19  46258  etransclem20  46259  etransclem21  46260  etransclem22  46261  etransclem23  46262  etransclem27  46266  etransclem32  46271  etransclem35  46274  etransclem46  46285  ioorrnopnlem  46309  ovnval2  46550  volicorecl  46551  hoiprodcl  46552  ovnf  46568  hsphoif  46581  hsphoival  46584  hoiprodcl3  46585  volicore  46586  hoidmvcl  46587  hsphoidmvle2  46590  hsphoidmvle  46591  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmvlelem2  46601  hoidmvlelem3  46602  ovnhoilem1  46606  hoidifhspf  46623  hoidifhspval3  46624  ovolval4lem1  46654  ovolval4lem2  46655  smfmullem1  46796  smfmullem2  46797  smfmullem3  46798  afv2ex  47219  suppmptcfin  48368  linc1  48418  lcoss  48429  el0ldep  48459