MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifcld Structured version   Visualization version   GIF version

Theorem ifcld 4533
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
StepHypRef Expression
1 ifcld.a . 2 (𝜑𝐴𝐶)
2 ifcld.b . 2 (𝜑𝐵𝐶)
3 ifcl 4532 . 2 ((𝐴𝐶𝐵𝐶) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
41, 2, 3syl2anc 585 1 (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  ifcif 4487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-if 4488
This theorem is referenced by:  ifexd  4535  soltmin  6091  pw2f1olem  9021  unxpdomlem3  9197  wemaplem2  9484  cantnfp1lem1  9615  cantnfp1lem2  9616  cantnfp1lem3  9617  cantnflem1d  9625  cantnflem1  9626  ssfzunsnext  13487  relexpsucnnr  14911  rexuzre  15238  rexico  15239  limsupgre  15364  rlim3  15381  o1lo1  15420  rlimclim1  15428  lo1resb  15447  o1resb  15449  o1of2  15496  o1rlimmul  15502  lo1le  15537  ruclem1  16114  ruclem10  16122  bitsfzo  16316  ramub1lem2  16900  ramcl  16902  prmocl  16907  prmop1  16911  prmdvdsprmo  16915  prmolefac  16919  prmodvdslcmf  16920  prmgapprmo  16935  setsstruct2  17047  wunress  17132  wunressOLD  17133  opifismgm  18515  mulgfval  18875  frgpuptf  19553  gsumzsplit  19705  gsummpt1n0  19743  xrsds  20843  uvcvvcl2  21197  uvcff  21200  snifpsrbag  21327  psr1cl  21374  subrgpsr  21391  mvrf  21396  mplmon  21439  mplmonmul  21440  mplcoe1  21441  evlslem3  21493  evlslem1  21495  coe1tmfv2  21649  gsummoncoe1  21678  mamumat1cl  21791  dmatmulcl  21852  scmatscmiddistr  21860  1mavmul  21900  marrepeval  21915  marrepcl  21916  marepveval  21920  marepvcl  21921  mdetrsca2  21956  mdetr0  21957  mdetrlin2  21959  mdetralt2  21961  mdetero  21962  mdetunilem2  21965  mdetunilem5  21968  mdetunilem6  21969  mdetunilem8  21971  mdetunilem9  21972  maducoeval2  21992  maduf  21993  madutpos  21994  madugsum  21995  gsummatr01lem3  22009  marep01ma  22012  smadiadetglem2  22024  monmatcollpw  22131  pmatcollpw3fi1lem1  22138  pmatcollpw3fi1lem2  22139  xkopt  23009  tsmssplit  23506  ssblex  23784  stdbdxmet  23874  stdbdmet  23875  stdbdbl  23876  stdbdmopn  23877  nlmvscnlem1  24053  tgioo  24162  xrsxmet  24175  icccmplem2  24189  ipcnlem1  24612  ivthlem2  24819  ovolicc2lem5  24888  ioombl1lem1  24925  ioombl1lem3  24927  ioombl1lem4  24928  mbfmax  25016  i1fres  25073  itg1climres  25082  mbfi1fseqlem3  25085  mbfi1fseqlem4  25086  mbfi1fseqlem5  25087  limcres  25253  dvferm1lem  25351  dvferm2lem  25353  dvlip2  25362  lhop1  25381  dvfsumrlim  25398  mdegaddle  25442  deg1addle2  25470  deg1sublt  25478  ply1divmo  25503  plyaddlem1  25577  plyaddlem  25579  coeaddlem  25613  dgradd2  25632  plydiveu  25661  abelthlem9  25802  logcnlem2  26001  logcnlem3  26002  cxpcn3lem  26103  lgamgulmlem4  26384  lgamgulmlem6  26386  ftalem2  26426  gausslemma2dlem4  26720  chebbnd1lem1  26820  dchrisumlem3  26842  dchrvmasumiflem1  26852  ostth3  26989  axlowdimlem15  27908  dstfrvunirn  33077  circlemeth  33256  indispconn  33831  ex-sategoelel  34018  ex-sategoelelomsuc  34023  knoppndvlem18  34995  itg2addnclem2  36133  itg2addnclem3  36134  ftc1anclem5  36158  sticksstones10  40566  sticksstones12a  40568  metakunt3  40582  metakunt4  40583  metakunt29  40608  metakunt30  40609  metakunt32  40611  metakunt33  40612  rhmmpl  40744  evlsbagval  40751  fsuppind  40768  fsuppssind  40771  mhpind  40772  mhphf  40774  dffltz  40975  irrapxlem4  41151  irrapxlem5  41152  kelac1  41393  areaquad  41553  cantnfresb  41661  sqrtcval  41920  clsk1indlem4  42323  mnringmulrcld  42515  refsum2cnlem1  43249  rexabslelem  43660  uzublem  43672  ioondisj2  43738  ioondisj1  43739  uzubioo  43812  mullimc  43864  mullimcf  43871  lptioo2  43879  limcleqr  43892  0ellimcdiv  43897  limsupubuzlem  43960  limsupequzmptlem  43976  climxrre  43998  limsup10exlem  44020  limsup10ex  44021  liminf10ex  44022  liminflelimsuplem  44023  icccncfext  44135  cncfiooicclem1  44141  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  stoweid  44311  fourierdlem9  44364  fourierdlem10  44365  fourierdlem37  44392  fourierdlem40  44395  fourierdlem66  44420  fourierdlem73  44427  fourierdlem74  44428  fourierdlem75  44429  fourierdlem78  44432  fourierdlem79  44433  fourierdlem95  44449  fourierdlem103  44457  sqwvfoura  44476  fouriersw  44479  etransclem1  44483  etransclem4  44486  etransclem17  44499  etransclem18  44500  etransclem19  44501  etransclem20  44502  etransclem21  44503  etransclem22  44504  etransclem23  44505  etransclem27  44509  etransclem32  44514  etransclem35  44517  etransclem46  44528  ioorrnopnlem  44552  ovnval2  44793  volicorecl  44794  hoiprodcl  44795  ovnf  44811  hsphoif  44824  hsphoival  44827  hoiprodcl3  44828  volicore  44829  hoidmvcl  44830  hsphoidmvle2  44833  hsphoidmvle  44834  hoidmv1lelem1  44839  hoidmv1lelem2  44840  hoidmv1lelem3  44841  hoidmvlelem2  44844  hoidmvlelem3  44845  ovnhoilem1  44849  hoidifhspf  44866  hoidifhspval3  44867  ovolval4lem1  44897  ovolval4lem2  44898  smfmullem1  45039  smfmullem2  45040  smfmullem3  45041  afv2ex  45453  suppmptcfin  46462  linc1  46513  lcoss  46524  el0ldep  46554
  Copyright terms: Public domain W3C validator