Theorem ifcld 4502

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

Syntax hints:   → wi 4   ∈ wcel 2119  ifcif 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-if 4456

This theorem is referenced by:  ifexd  4504  soltmin  6087  pw2f1olem  9010  unxpdomlem3  9159  wemaplem2  9453  cantnfp1lem1  9591  cantnfp1lem2  9592  cantnfp1lem3  9593  cantnflem1d  9601  cantnflem1  9602  ssfzunsnext  13515  tpf  14453  relexpsucnnr  14979  rexuzre  15307  rexico  15308  limsupgre  15435  rlim3  15452  o1lo1  15491  rlimclim1  15499  lo1resb  15518  o1resb  15520  o1of2  15567  o1rlimmul  15573  lo1le  15606  ruclem1  16190  ruclem10  16198  bitsfzo  16396  ramub1lem2  16990  ramcl  16992  prmocl  16997  prmop1  17001  prmdvdsprmo  17005  prmolefac  17009  prmodvdslcmf  17010  prmgapprmo  17025  setsstruct2  17136  wunress  17211  opifismgm  18619  mulgfval  19037  frgpuptf  19737  gsumzsplit  19894  gsummpt1n0  19932  xrsds  21386  uvcvvcl2  21764  uvcff  21767  snifpsrbag  21896  psr1cl  21936  subrgpsr  21953  mvrf  21960  mplmon  22012  mplmonmul  22013  mplcoe1  22014  evlslem3  22057  evlslem1  22059  selvvvval  22119  coe1tmfv2  22262  gsummoncoe1  22295  rhmmpl  22367  rhmply1vr1  22371  mamumat1cl  22423  dmatmulcl  22484  scmatscmiddistr  22492  1mavmul  22532  marrepeval  22547  marrepcl  22548  marepveval  22552  marepvcl  22553  mdetrsca2  22588  mdetr0  22589  mdetrlin2  22591  mdetralt2  22593  mdetero  22594  mdetunilem2  22597  mdetunilem5  22600  mdetunilem6  22601  mdetunilem8  22603  mdetunilem9  22604  maducoeval2  22624  maduf  22625  madutpos  22626  madugsum  22627  gsummatr01lem3  22641  marep01ma  22644  smadiadetglem2  22656  monmatcollpw  22763  pmatcollpw3fi1lem1  22770  pmatcollpw3fi1lem2  22771  xkopt  23639  tsmssplit  24136  ssblex  24412  stdbdxmet  24499  stdbdmet  24500  stdbdbl  24501  stdbdmopn  24502  nlmvscnlem1  24670  tgioo  24780  xrsxmet  24794  icccmplem2  24808  ipcnlem1  25231  ivthlem2  25438  ovolicc2lem5  25507  ioombl1lem1  25544  ioombl1lem3  25546  ioombl1lem4  25547  mbfmax  25635  i1fres  25691  itg1climres  25700  mbfi1fseqlem3  25703  mbfi1fseqlem4  25704  mbfi1fseqlem5  25705  limcres  25872  dvferm1lem  25970  dvferm2lem  25972  dvlip2  25981  lhop1  26000  dvfsumrlim  26017  mdegaddle  26058  deg1addle2  26086  deg1sublt  26094  ply1divmo  26120  plyaddlem1  26197  plyaddlem  26199  coeaddlem  26233  dgradd2  26252  plydiveu  26283  abelthlem9  26424  logcnlem2  26626  logcnlem3  26627  cxpcn3lem  26730  lgamgulmlem4  27014  lgamgulmlem6  27016  ftalem2  27056  gausslemma2dlem4  27351  chebbnd1lem1  27451  dchrisumlem3  27473  dchrvmasumiflem1  27483  ostth3  27620  abssval  28250  absscl  28251  axlowdimlem15  29044  elrspunsn  33513  ply1moneq  33680  deg1addlt  33692  mplasclco  33709  selvply1rhmlem2  33714  extvfvv  33727  extvfvvcl  33728  extvfvcl  33729  mplvrpmrhm  33740  psrmon  33742  psrmonmul  33743  psrmonprod  33745  mplmonprod  33747  esplyfval0  33757  esplyfval1  33766  esplyind  33768  fldextrspunlsp  33867  dstfrvunirn  34668  circlemeth  34833  indispconn  35471  ex-sategoelel  35658  ex-sategoelelomsuc  35663  knoppndvlem18  36844  itg2addnclem2  38048  itg2addnclem3  38049  ftc1anclem5  38073  sticksstones10  42649  sticksstones12a  42651  aks6d1c6lem3  42666  rhmpsr  43042  evlsbagval  43045  fsuppind  43049  fsuppssind  43052  mhpind  43053  dffltz  43093  irrapxlem4  43279  irrapxlem5  43280  kelac1  43517  areaquad  43670  cantnfresb  43778  sqrtcval  44094  clsk1indlem4  44497  mnringmulrcld  44681  refsum2cnlem1  45494  rexabslelem  45869  uzublem  45881  ioondisj2  45946  ioondisj1  45947  uzubioo  46018  mullimc  46069  mullimcf  46076  lptioo2  46084  limcleqr  46095  0ellimcdiv  46100  limsupubuzlem  46163  limsupequzmptlem  46179  climxrre  46201  limsup10exlem  46223  limsup10ex  46224  liminf10ex  46225  liminflelimsuplem  46226  icccncfext  46338  cncfiooicclem1  46344  ioodvbdlimc1lem2  46383  ioodvbdlimc2lem  46385  stoweid  46514  fourierdlem9  46567  fourierdlem10  46568  fourierdlem37  46595  fourierdlem40  46598  fourierdlem66  46623  fourierdlem73  46630  fourierdlem74  46631  fourierdlem75  46632  fourierdlem78  46635  fourierdlem79  46636  fourierdlem95  46652  fourierdlem103  46660  sqwvfoura  46679  fouriersw  46682  etransclem1  46686  etransclem4  46689  etransclem17  46702  etransclem18  46703  etransclem19  46704  etransclem20  46705  etransclem21  46706  etransclem22  46707  etransclem23  46708  etransclem27  46712  etransclem32  46717  etransclem35  46720  etransclem46  46731  ioorrnopnlem  46755  ovnval2  46996  volicorecl  46997  hoiprodcl  46998  ovnf  47014  hsphoif  47027  hsphoival  47030  hoiprodcl3  47031  volicore  47032  hoidmvcl  47033  hsphoidmvle2  47036  hsphoidmvle  47037  hoidmv1lelem1  47042  hoidmv1lelem2  47043  hoidmv1lelem3  47044  hoidmvlelem2  47047  hoidmvlelem3  47048  ovnhoilem1  47052  hoidifhspf  47069  hoidifhspval3  47070  ovolval4lem1  47100  ovolval4lem2  47101  smfmullem1  47242  smfmullem2  47243  smfmullem3  47244  afv2ex  47685  suppmptcfin  48875  linc1  48924  lcoss  48935  el0ldep  48965