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

Theorem ifcld 4515
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 4514 . 2 ((𝐴𝐶𝐵𝐶) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
41, 2, 3syl2anc 584 1 (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  ifcif 4470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-ex 1774  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-if 4471
This theorem is referenced by:  soltmin  5995  pw2f1olem  8615  unxpdomlem3  8718  wemaplem2  9005  cantnfp1lem1  9135  cantnfp1lem2  9136  cantnfp1lem3  9137  cantnflem1d  9145  cantnflem1  9146  ssfzunsnext  12947  relexpsucnnr  14379  rexuzre  14707  rexico  14708  limsupgre  14833  rlim3  14850  o1lo1  14889  rlimclim1  14897  lo1resb  14916  o1resb  14918  o1of2  14964  o1rlimmul  14970  lo1le  15003  ruclem1  15579  ruclem10  15587  bitsfzo  15779  ramub1lem2  16358  ramcl  16360  prmocl  16365  prmop1  16369  prmdvdsprmo  16373  prmolefac  16377  prmodvdslcmf  16378  prmgapprmo  16393  setsstruct2  16516  wunress  16559  opifismgm  17864  mulgfval  18171  frgpuptf  18832  gsumzsplit  18983  gsummpt1n0  19021  snifpsrbag  20081  psr1cl  20117  subrgpsr  20134  mvrf  20139  mplmon  20179  mplmonmul  20180  mplcoe1  20181  evlslem3  20228  evlslem1  20230  coe1tmfv2  20378  gsummoncoe1  20407  xrsds  20523  uvcvvcl2  20867  uvcff  20870  mamumat1cl  20983  dmatmulcl  21044  scmatscmiddistr  21052  1mavmul  21092  marrepeval  21107  marrepcl  21108  marepveval  21112  marepvcl  21113  mdetrsca2  21148  mdetr0  21149  mdetrlin2  21151  mdetralt2  21153  mdetero  21154  mdetunilem2  21157  mdetunilem5  21160  mdetunilem6  21161  mdetunilem8  21163  mdetunilem9  21164  maducoeval2  21184  maduf  21185  madutpos  21186  madugsum  21187  gsummatr01lem3  21201  marep01ma  21204  smadiadetglem2  21216  monmatcollpw  21322  pmatcollpw3fi1lem1  21329  pmatcollpw3fi1lem2  21330  xkopt  22198  tsmssplit  22694  ssblex  22972  stdbdxmet  23059  stdbdmet  23060  stdbdbl  23061  stdbdmopn  23062  nlmvscnlem1  23229  tgioo  23338  xrsxmet  23351  icccmplem2  23365  ipcnlem1  23782  ivthlem2  23987  ovolicc2lem5  24056  ioombl1lem1  24093  ioombl1lem3  24095  ioombl1lem4  24096  mbfmax  24184  i1fres  24240  itg1climres  24249  mbfi1fseqlem3  24252  mbfi1fseqlem4  24253  mbfi1fseqlem5  24254  limcres  24418  dvferm1lem  24515  dvferm2lem  24517  dvlip2  24526  lhop1  24545  dvfsumrlim  24562  mdegaddle  24602  deg1addle2  24630  deg1sublt  24638  ply1divmo  24663  plyaddlem1  24737  plyaddlem  24739  coeaddlem  24773  dgradd2  24792  plydiveu  24821  abelthlem9  24962  logcnlem2  25158  logcnlem3  25159  cxpcn3lem  25260  lgamgulmlem4  25542  lgamgulmlem6  25544  ftalem2  25584  gausslemma2dlem4  25878  chebbnd1lem1  25978  dchrisumlem3  26000  dchrvmasumiflem1  26010  ostth3  26147  axlowdimlem15  26675  dstfrvunirn  31637  circlemeth  31816  indispconn  32384  ex-sategoelel  32571  ex-sategoelelomsuc  32576  noprefixmo  33105  knoppndvlem18  33771  itg2addnclem2  34830  itg2addnclem3  34831  ftc1anclem5  34857  dffltz  39155  irrapxlem4  39306  irrapxlem5  39307  kelac1  39547  areaquad  39707  clsk1indlem4  40278  refsum2cnlem1  41178  rexabslelem  41576  uzublem  41588  ioondisj2  41651  ioondisj1  41652  uzubioo  41727  mullimc  41781  mullimcf  41788  lptioo2  41796  limcleqr  41809  0ellimcdiv  41814  limsupubuzlem  41877  limsupequzmptlem  41893  climxrre  41915  limsup10exlem  41937  limsup10ex  41938  liminf10ex  41939  liminflelimsuplem  41940  icccncfext  42054  cncfiooicclem1  42060  ioodvbdlimc1lem2  42101  ioodvbdlimc2lem  42103  stoweid  42233  fourierdlem9  42286  fourierdlem10  42287  fourierdlem37  42314  fourierdlem40  42317  fourierdlem66  42342  fourierdlem73  42349  fourierdlem74  42350  fourierdlem75  42351  fourierdlem78  42354  fourierdlem79  42355  fourierdlem95  42371  fourierdlem103  42379  sqwvfoura  42398  fouriersw  42401  etransclem1  42405  etransclem4  42408  etransclem17  42421  etransclem18  42422  etransclem19  42423  etransclem20  42424  etransclem21  42425  etransclem22  42426  etransclem23  42427  etransclem27  42431  etransclem32  42436  etransclem35  42439  etransclem46  42450  ioorrnopnlem  42474  ovnval2  42712  volicorecl  42713  hoiprodcl  42714  ovnf  42730  hsphoif  42743  hsphoival  42746  hoiprodcl3  42747  volicore  42748  hoidmvcl  42749  hsphoidmvle2  42752  hsphoidmvle  42753  hoidmv1lelem1  42758  hoidmv1lelem2  42759  hoidmv1lelem3  42760  hoidmvlelem2  42763  hoidmvlelem3  42764  ovnhoilem1  42768  hoidifhspf  42785  hoidifhspval3  42786  ovolval4lem1  42816  ovolval4lem2  42817  smfmullem1  42951  smfmullem2  42952  smfmullem3  42953  afv2ex  43298  suppmptcfin  44329  linc1  44382  lcoss  44393  el0ldep  44423
  Copyright terms: Public domain W3C validator