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

Theorem ifcld 4506
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 4505 . 2 ((𝐴𝐶𝐵𝐶) → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
41, 2, 3syl2anc 584 1 (𝜑 → if(𝜓, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  ifcif 4460
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 2710
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-if 4461
This theorem is referenced by:  ifexd  4508  soltmin  6046  pw2f1olem  8872  unxpdomlem3  9038  wemaplem2  9315  cantnfp1lem1  9445  cantnfp1lem2  9446  cantnfp1lem3  9447  cantnflem1d  9455  cantnflem1  9456  ssfzunsnext  13310  relexpsucnnr  14745  rexuzre  15073  rexico  15074  limsupgre  15199  rlim3  15216  o1lo1  15255  rlimclim1  15263  lo1resb  15282  o1resb  15284  o1of2  15331  o1rlimmul  15337  lo1le  15372  ruclem1  15949  ruclem10  15957  bitsfzo  16151  ramub1lem2  16737  ramcl  16739  prmocl  16744  prmop1  16748  prmdvdsprmo  16752  prmolefac  16756  prmodvdslcmf  16757  prmgapprmo  16772  setsstruct2  16884  wunress  16969  wunressOLD  16970  opifismgm  18352  mulgfval  18711  frgpuptf  19385  gsumzsplit  19537  gsummpt1n0  19575  xrsds  20650  uvcvvcl2  21004  uvcff  21007  snifpsrbag  21134  psr1cl  21180  subrgpsr  21197  mvrf  21202  mplmon  21245  mplmonmul  21246  mplcoe1  21247  evlslem3  21299  evlslem1  21301  coe1tmfv2  21455  gsummoncoe1  21484  mamumat1cl  21597  dmatmulcl  21658  scmatscmiddistr  21666  1mavmul  21706  marrepeval  21721  marrepcl  21722  marepveval  21726  marepvcl  21727  mdetrsca2  21762  mdetr0  21763  mdetrlin2  21765  mdetralt2  21767  mdetero  21768  mdetunilem2  21771  mdetunilem5  21774  mdetunilem6  21775  mdetunilem8  21777  mdetunilem9  21778  maducoeval2  21798  maduf  21799  madutpos  21800  madugsum  21801  gsummatr01lem3  21815  marep01ma  21818  smadiadetglem2  21830  monmatcollpw  21937  pmatcollpw3fi1lem1  21944  pmatcollpw3fi1lem2  21945  xkopt  22815  tsmssplit  23312  ssblex  23590  stdbdxmet  23680  stdbdmet  23681  stdbdbl  23682  stdbdmopn  23683  nlmvscnlem1  23859  tgioo  23968  xrsxmet  23981  icccmplem2  23995  ipcnlem1  24418  ivthlem2  24625  ovolicc2lem5  24694  ioombl1lem1  24731  ioombl1lem3  24733  ioombl1lem4  24734  mbfmax  24822  i1fres  24879  itg1climres  24888  mbfi1fseqlem3  24891  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  limcres  25059  dvferm1lem  25157  dvferm2lem  25159  dvlip2  25168  lhop1  25187  dvfsumrlim  25204  mdegaddle  25248  deg1addle2  25276  deg1sublt  25284  ply1divmo  25309  plyaddlem1  25383  plyaddlem  25385  coeaddlem  25419  dgradd2  25438  plydiveu  25467  abelthlem9  25608  logcnlem2  25807  logcnlem3  25808  cxpcn3lem  25909  lgamgulmlem4  26190  lgamgulmlem6  26192  ftalem2  26232  gausslemma2dlem4  26526  chebbnd1lem1  26626  dchrisumlem3  26648  dchrvmasumiflem1  26658  ostth3  26795  axlowdimlem15  27333  dstfrvunirn  32450  circlemeth  32629  indispconn  33205  ex-sategoelel  33392  ex-sategoelelomsuc  33397  knoppndvlem18  34718  itg2addnclem2  35838  itg2addnclem3  35839  ftc1anclem5  35863  sticksstones10  40118  sticksstones12a  40120  metakunt3  40134  metakunt4  40135  metakunt29  40160  metakunt30  40161  metakunt32  40163  metakunt33  40164  evlsbagval  40282  fsuppind  40286  fsuppssind  40289  mhpind  40290  mhphf  40292  dffltz  40478  irrapxlem4  40654  irrapxlem5  40655  kelac1  40895  areaquad  41054  sqrtcval  41256  clsk1indlem4  41661  mnringmulrcld  41853  refsum2cnlem1  42587  rexabslelem  42965  uzublem  42977  ioondisj2  43038  ioondisj1  43039  uzubioo  43112  mullimc  43164  mullimcf  43171  lptioo2  43179  limcleqr  43192  0ellimcdiv  43197  limsupubuzlem  43260  limsupequzmptlem  43276  climxrre  43298  limsup10exlem  43320  limsup10ex  43321  liminf10ex  43322  liminflelimsuplem  43323  icccncfext  43435  cncfiooicclem1  43441  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  stoweid  43611  fourierdlem9  43664  fourierdlem10  43665  fourierdlem37  43692  fourierdlem40  43695  fourierdlem66  43720  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem78  43732  fourierdlem79  43733  fourierdlem95  43749  fourierdlem103  43757  sqwvfoura  43776  fouriersw  43779  etransclem1  43783  etransclem4  43786  etransclem17  43799  etransclem18  43800  etransclem19  43801  etransclem20  43802  etransclem21  43803  etransclem22  43804  etransclem23  43805  etransclem27  43809  etransclem32  43814  etransclem35  43817  etransclem46  43828  ioorrnopnlem  43852  ovnval2  44090  volicorecl  44091  hoiprodcl  44092  ovnf  44108  hsphoif  44121  hsphoival  44124  hoiprodcl3  44125  volicore  44126  hoidmvcl  44127  hsphoidmvle2  44130  hsphoidmvle  44131  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmvlelem2  44141  hoidmvlelem3  44142  ovnhoilem1  44146  hoidifhspf  44163  hoidifhspval3  44164  ovolval4lem1  44194  ovolval4lem2  44195  smfmullem1  44336  smfmullem2  44337  smfmullem3  44338  afv2ex  44717  suppmptcfin  45726  linc1  45777  lcoss  45788  el0ldep  45818
  Copyright terms: Public domain W3C validator