Theorem ifcld 4535

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

Syntax hints:   → wi 4   ∈ wcel 2109  ifcif 4488

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  ifexd  4537  soltmin  6109  pw2f1olem  9045  unxpdomlem3  9199  wemaplem2  9500  cantnfp1lem1  9631  cantnfp1lem2  9632  cantnfp1lem3  9633  cantnflem1d  9641  cantnflem1  9642  ssfzunsnext  13530  tpf  14464  relexpsucnnr  14991  rexuzre  15319  rexico  15320  limsupgre  15447  rlim3  15464  o1lo1  15503  rlimclim1  15511  lo1resb  15530  o1resb  15532  o1of2  15579  o1rlimmul  15585  lo1le  15618  ruclem1  16199  ruclem10  16207  bitsfzo  16405  ramub1lem2  16998  ramcl  17000  prmocl  17005  prmop1  17009  prmdvdsprmo  17013  prmolefac  17017  prmodvdslcmf  17018  prmgapprmo  17033  setsstruct2  17144  wunress  17219  opifismgm  18586  mulgfval  19001  frgpuptf  19700  gsumzsplit  19857  gsummpt1n0  19895  xrsds  21326  uvcvvcl2  21697  uvcff  21700  snifpsrbag  21829  psr1cl  21870  subrgpsr  21887  mvrf  21894  mplmon  21942  mplmonmul  21943  mplcoe1  21944  evlslem3  21987  evlslem1  21989  coe1tmfv2  22161  gsummoncoe1  22195  rhmmpl  22270  rhmply1vr1  22274  mamumat1cl  22326  dmatmulcl  22387  scmatscmiddistr  22395  1mavmul  22435  marrepeval  22450  marrepcl  22451  marepveval  22455  marepvcl  22456  mdetrsca2  22491  mdetr0  22492  mdetrlin2  22494  mdetralt2  22496  mdetero  22497  mdetunilem2  22500  mdetunilem5  22503  mdetunilem6  22504  mdetunilem8  22506  mdetunilem9  22507  maducoeval2  22527  maduf  22528  madutpos  22529  madugsum  22530  gsummatr01lem3  22544  marep01ma  22547  smadiadetglem2  22559  monmatcollpw  22666  pmatcollpw3fi1lem1  22673  pmatcollpw3fi1lem2  22674  xkopt  23542  tsmssplit  24039  ssblex  24316  stdbdxmet  24403  stdbdmet  24404  stdbdbl  24405  stdbdmopn  24406  nlmvscnlem1  24574  tgioo  24684  xrsxmet  24698  icccmplem2  24712  ipcnlem1  25145  ivthlem2  25353  ovolicc2lem5  25422  ioombl1lem1  25459  ioombl1lem3  25461  ioombl1lem4  25462  mbfmax  25550  i1fres  25606  itg1climres  25615  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  limcres  25787  dvferm1lem  25888  dvferm2lem  25890  dvlip2  25900  lhop1  25919  dvfsumrlim  25938  mdegaddle  25979  deg1addle2  26007  deg1sublt  26015  ply1divmo  26041  plyaddlem1  26118  plyaddlem  26120  coeaddlem  26154  dgradd2  26174  plydiveu  26206  abelthlem9  26350  logcnlem2  26552  logcnlem3  26553  cxpcn3lem  26657  lgamgulmlem4  26942  lgamgulmlem6  26944  ftalem2  26984  gausslemma2dlem4  27280  chebbnd1lem1  27380  dchrisumlem3  27402  dchrvmasumiflem1  27412  ostth3  27549  abssval  28141  absscl  28142  axlowdimlem15  28883  elrspunsn  33400  ply1moneq  33555  deg1addlt  33565  fldextrspunlsp  33669  dstfrvunirn  34466  circlemeth  34631  indispconn  35221  ex-sategoelel  35408  ex-sategoelelomsuc  35413  knoppndvlem18  36517  itg2addnclem2  37666  itg2addnclem3  37667  ftc1anclem5  37691  sticksstones10  42143  sticksstones12a  42145  aks6d1c6lem3  42160  rhmpsr  42540  evlsbagval  42554  selvvvval  42573  fsuppind  42578  fsuppssind  42581  mhpind  42582  dffltz  42622  irrapxlem4  42813  irrapxlem5  42814  kelac1  43052  areaquad  43205  cantnfresb  43313  sqrtcval  43630  clsk1indlem4  44033  mnringmulrcld  44217  refsum2cnlem1  45031  rexabslelem  45414  uzublem  45426  ioondisj2  45491  ioondisj1  45492  uzubioo  45563  mullimc  45614  mullimcf  45621  lptioo2  45629  limcleqr  45642  0ellimcdiv  45647  limsupubuzlem  45710  limsupequzmptlem  45726  climxrre  45748  limsup10exlem  45770  limsup10ex  45771  liminf10ex  45772  liminflelimsuplem  45773  icccncfext  45885  cncfiooicclem1  45891  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  stoweid  46061  fourierdlem9  46114  fourierdlem10  46115  fourierdlem37  46142  fourierdlem40  46145  fourierdlem66  46170  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem78  46182  fourierdlem79  46183  fourierdlem95  46199  fourierdlem103  46207  sqwvfoura  46226  fouriersw  46229  etransclem1  46233  etransclem4  46236  etransclem17  46249  etransclem18  46250  etransclem19  46251  etransclem20  46252  etransclem21  46253  etransclem22  46254  etransclem23  46255  etransclem27  46259  etransclem32  46264  etransclem35  46267  etransclem46  46278  ioorrnopnlem  46302  ovnval2  46543  volicorecl  46544  hoiprodcl  46545  ovnf  46561  hsphoif  46574  hsphoival  46577  hoiprodcl3  46578  volicore  46579  hoidmvcl  46580  hsphoidmvle2  46583  hsphoidmvle  46584  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmvlelem2  46594  hoidmvlelem3  46595  ovnhoilem1  46599  hoidifhspf  46616  hoidifhspval3  46617  ovolval4lem1  46647  ovolval4lem2  46648  smfmullem1  46789  smfmullem2  46790  smfmullem3  46791  afv2ex  47215  suppmptcfin  48364  linc1  48414  lcoss  48425  el0ldep  48455