Theorem ifcld 4531

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

Syntax hints:   → wi 4   ∈ wcel 2109  ifcif 4484

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 4485

This theorem is referenced by:  ifexd  4533  soltmin  6097  pw2f1olem  9022  unxpdomlem3  9175  wemaplem2  9476  cantnfp1lem1  9607  cantnfp1lem2  9608  cantnfp1lem3  9609  cantnflem1d  9617  cantnflem1  9618  ssfzunsnext  13506  tpf  14440  relexpsucnnr  14967  rexuzre  15295  rexico  15296  limsupgre  15423  rlim3  15440  o1lo1  15479  rlimclim1  15487  lo1resb  15506  o1resb  15508  o1of2  15555  o1rlimmul  15561  lo1le  15594  ruclem1  16175  ruclem10  16183  bitsfzo  16381  ramub1lem2  16974  ramcl  16976  prmocl  16981  prmop1  16985  prmdvdsprmo  16989  prmolefac  16993  prmodvdslcmf  16994  prmgapprmo  17009  setsstruct2  17120  wunress  17195  opifismgm  18568  mulgfval  18983  frgpuptf  19684  gsumzsplit  19841  gsummpt1n0  19879  xrsds  21351  uvcvvcl2  21730  uvcff  21733  snifpsrbag  21862  psr1cl  21903  subrgpsr  21920  mvrf  21927  mplmon  21975  mplmonmul  21976  mplcoe1  21977  evlslem3  22020  evlslem1  22022  coe1tmfv2  22194  gsummoncoe1  22228  rhmmpl  22303  rhmply1vr1  22307  mamumat1cl  22359  dmatmulcl  22420  scmatscmiddistr  22428  1mavmul  22468  marrepeval  22483  marrepcl  22484  marepveval  22488  marepvcl  22489  mdetrsca2  22524  mdetr0  22525  mdetrlin2  22527  mdetralt2  22529  mdetero  22530  mdetunilem2  22533  mdetunilem5  22536  mdetunilem6  22537  mdetunilem8  22539  mdetunilem9  22540  maducoeval2  22560  maduf  22561  madutpos  22562  madugsum  22563  gsummatr01lem3  22577  marep01ma  22580  smadiadetglem2  22592  monmatcollpw  22699  pmatcollpw3fi1lem1  22706  pmatcollpw3fi1lem2  22707  xkopt  23575  tsmssplit  24072  ssblex  24349  stdbdxmet  24436  stdbdmet  24437  stdbdbl  24438  stdbdmopn  24439  nlmvscnlem1  24607  tgioo  24717  xrsxmet  24731  icccmplem2  24745  ipcnlem1  25178  ivthlem2  25386  ovolicc2lem5  25455  ioombl1lem1  25492  ioombl1lem3  25494  ioombl1lem4  25495  mbfmax  25583  i1fres  25639  itg1climres  25648  mbfi1fseqlem3  25651  mbfi1fseqlem4  25652  mbfi1fseqlem5  25653  limcres  25820  dvferm1lem  25921  dvferm2lem  25923  dvlip2  25933  lhop1  25952  dvfsumrlim  25971  mdegaddle  26012  deg1addle2  26040  deg1sublt  26048  ply1divmo  26074  plyaddlem1  26151  plyaddlem  26153  coeaddlem  26187  dgradd2  26207  plydiveu  26239  abelthlem9  26383  logcnlem2  26585  logcnlem3  26586  cxpcn3lem  26690  lgamgulmlem4  26975  lgamgulmlem6  26977  ftalem2  27017  gausslemma2dlem4  27313  chebbnd1lem1  27413  dchrisumlem3  27435  dchrvmasumiflem1  27445  ostth3  27582  abssval  28181  absscl  28182  axlowdimlem15  28936  elrspunsn  33393  ply1moneq  33548  deg1addlt  33558  fldextrspunlsp  33662  dstfrvunirn  34459  circlemeth  34624  indispconn  35214  ex-sategoelel  35401  ex-sategoelelomsuc  35406  knoppndvlem18  36510  itg2addnclem2  37659  itg2addnclem3  37660  ftc1anclem5  37684  sticksstones10  42136  sticksstones12a  42138  aks6d1c6lem3  42153  rhmpsr  42533  evlsbagval  42547  selvvvval  42566  fsuppind  42571  fsuppssind  42574  mhpind  42575  dffltz  42615  irrapxlem4  42806  irrapxlem5  42807  kelac1  43045  areaquad  43198  cantnfresb  43306  sqrtcval  43623  clsk1indlem4  44026  mnringmulrcld  44210  refsum2cnlem1  45024  rexabslelem  45407  uzublem  45419  ioondisj2  45484  ioondisj1  45485  uzubioo  45556  mullimc  45607  mullimcf  45614  lptioo2  45622  limcleqr  45635  0ellimcdiv  45640  limsupubuzlem  45703  limsupequzmptlem  45719  climxrre  45741  limsup10exlem  45763  limsup10ex  45764  liminf10ex  45765  liminflelimsuplem  45766  icccncfext  45878  cncfiooicclem1  45884  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  stoweid  46054  fourierdlem9  46107  fourierdlem10  46108  fourierdlem37  46135  fourierdlem40  46138  fourierdlem66  46163  fourierdlem73  46170  fourierdlem74  46171  fourierdlem75  46172  fourierdlem78  46175  fourierdlem79  46176  fourierdlem95  46192  fourierdlem103  46200  sqwvfoura  46219  fouriersw  46222  etransclem1  46226  etransclem4  46229  etransclem17  46242  etransclem18  46243  etransclem19  46244  etransclem20  46245  etransclem21  46246  etransclem22  46247  etransclem23  46248  etransclem27  46252  etransclem32  46257  etransclem35  46260  etransclem46  46271  ioorrnopnlem  46295  ovnval2  46536  volicorecl  46537  hoiprodcl  46538  ovnf  46554  hsphoif  46567  hsphoival  46570  hoiprodcl3  46571  volicore  46572  hoidmvcl  46573  hsphoidmvle2  46576  hsphoidmvle  46577  hoidmv1lelem1  46582  hoidmv1lelem2  46583  hoidmv1lelem3  46584  hoidmvlelem2  46587  hoidmvlelem3  46588  ovnhoilem1  46592  hoidifhspf  46609  hoidifhspval3  46610  ovolval4lem1  46640  ovolval4lem2  46641  smfmullem1  46782  smfmullem2  46783  smfmullem3  46784  afv2ex  47208  suppmptcfin  48357  linc1  48407  lcoss  48418  el0ldep  48448