Theorem ifcld 4576

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

Syntax hints:   → wi 4   ∈ wcel 2105  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-if 4531

This theorem is referenced by:  ifexd  4578  soltmin  6158  pw2f1olem  9114  unxpdomlem3  9285  wemaplem2  9584  cantnfp1lem1  9715  cantnfp1lem2  9716  cantnfp1lem3  9717  cantnflem1d  9725  cantnflem1  9726  ssfzunsnext  13605  tpf  14534  relexpsucnnr  15060  rexuzre  15387  rexico  15388  limsupgre  15513  rlim3  15530  o1lo1  15569  rlimclim1  15577  lo1resb  15596  o1resb  15598  o1of2  15645  o1rlimmul  15651  lo1le  15684  ruclem1  16263  ruclem10  16271  bitsfzo  16468  ramub1lem2  17060  ramcl  17062  prmocl  17067  prmop1  17071  prmdvdsprmo  17075  prmolefac  17079  prmodvdslcmf  17080  prmgapprmo  17095  setsstruct2  17207  wunress  17295  wunressOLD  17296  opifismgm  18684  mulgfval  19099  frgpuptf  19802  gsumzsplit  19959  gsummpt1n0  19997  xrsds  21444  uvcvvcl2  21825  uvcff  21828  snifpsrbag  21957  psr1cl  21998  subrgpsr  22015  mvrf  22022  mplmon  22070  mplmonmul  22071  mplcoe1  22072  evlslem3  22121  evlslem1  22123  coe1tmfv2  22293  gsummoncoe1  22327  rhmmpl  22402  rhmply1vr1  22406  mamumat1cl  22460  dmatmulcl  22521  scmatscmiddistr  22529  1mavmul  22569  marrepeval  22584  marrepcl  22585  marepveval  22589  marepvcl  22590  mdetrsca2  22625  mdetr0  22626  mdetrlin2  22628  mdetralt2  22630  mdetero  22631  mdetunilem2  22634  mdetunilem5  22637  mdetunilem6  22638  mdetunilem8  22640  mdetunilem9  22641  maducoeval2  22661  maduf  22662  madutpos  22663  madugsum  22664  gsummatr01lem3  22678  marep01ma  22681  smadiadetglem2  22693  monmatcollpw  22800  pmatcollpw3fi1lem1  22807  pmatcollpw3fi1lem2  22808  xkopt  23678  tsmssplit  24175  ssblex  24453  stdbdxmet  24543  stdbdmet  24544  stdbdbl  24545  stdbdmopn  24546  nlmvscnlem1  24722  tgioo  24831  xrsxmet  24844  icccmplem2  24858  ipcnlem1  25292  ivthlem2  25500  ovolicc2lem5  25569  ioombl1lem1  25606  ioombl1lem3  25608  ioombl1lem4  25609  mbfmax  25697  i1fres  25754  itg1climres  25763  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  limcres  25935  dvferm1lem  26036  dvferm2lem  26038  dvlip2  26048  lhop1  26067  dvfsumrlim  26086  mdegaddle  26127  deg1addle2  26155  deg1sublt  26163  ply1divmo  26189  plyaddlem1  26266  plyaddlem  26268  coeaddlem  26302  dgradd2  26322  plydiveu  26354  abelthlem9  26498  logcnlem2  26699  logcnlem3  26700  cxpcn3lem  26804  lgamgulmlem4  27089  lgamgulmlem6  27091  ftalem2  27131  gausslemma2dlem4  27427  chebbnd1lem1  27527  dchrisumlem3  27549  dchrvmasumiflem1  27559  ostth3  27696  abssval  28277  absscl  28278  axlowdimlem15  28985  elrspunsn  33436  ply1moneq  33590  deg1addlt  33599  dstfrvunirn  34455  circlemeth  34633  indispconn  35218  ex-sategoelel  35405  ex-sategoelelomsuc  35410  knoppndvlem18  36511  itg2addnclem2  37658  itg2addnclem3  37659  ftc1anclem5  37683  sticksstones10  42136  sticksstones12a  42138  aks6d1c6lem3  42153  metakunt3  42188  metakunt4  42189  metakunt29  42214  metakunt30  42215  metakunt32  42217  metakunt33  42218  rhmpsr  42538  evlsbagval  42552  selvvvval  42571  fsuppind  42576  fsuppssind  42579  mhpind  42580  dffltz  42620  irrapxlem4  42812  irrapxlem5  42813  kelac1  43051  areaquad  43204  cantnfresb  43313  sqrtcval  43630  clsk1indlem4  44033  mnringmulrcld  44223  refsum2cnlem1  44974  rexabslelem  45367  uzublem  45379  ioondisj2  45445  ioondisj1  45446  uzubioo  45519  mullimc  45571  mullimcf  45578  lptioo2  45586  limcleqr  45599  0ellimcdiv  45604  limsupubuzlem  45667  limsupequzmptlem  45683  climxrre  45705  limsup10exlem  45727  limsup10ex  45728  liminf10ex  45729  liminflelimsuplem  45730  icccncfext  45842  cncfiooicclem1  45848  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  stoweid  46018  fourierdlem9  46071  fourierdlem10  46072  fourierdlem37  46099  fourierdlem40  46102  fourierdlem66  46127  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem78  46139  fourierdlem79  46140  fourierdlem95  46156  fourierdlem103  46164  sqwvfoura  46183  fouriersw  46186  etransclem1  46190  etransclem4  46193  etransclem17  46206  etransclem18  46207  etransclem19  46208  etransclem20  46209  etransclem21  46210  etransclem22  46211  etransclem23  46212  etransclem27  46216  etransclem32  46221  etransclem35  46224  etransclem46  46235  ioorrnopnlem  46259  ovnval2  46500  volicorecl  46501  hoiprodcl  46502  ovnf  46518  hsphoif  46531  hsphoival  46534  hoiprodcl3  46535  volicore  46536  hoidmvcl  46537  hsphoidmvle2  46540  hsphoidmvle  46541  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmvlelem2  46551  hoidmvlelem3  46552  ovnhoilem1  46556  hoidifhspf  46573  hoidifhspval3  46574  ovolval4lem1  46604  ovolval4lem2  46605  smfmullem1  46746  smfmullem2  46747  smfmullem3  46748  afv2ex  47163  suppmptcfin  48220  linc1  48270  lcoss  48281  el0ldep  48311