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

Theorem ifcl 4079
Description: Membership (closure) of a conditional operator. (Contributed by NM, 4-Apr-2005.)
Assertion
Ref Expression
ifcl ((𝐴𝐶𝐵𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)

Proof of Theorem ifcl
StepHypRef Expression
1 eleq1 2675 . 2 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝐴𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
2 eleq1 2675 . 2 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝐵𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
31, 2ifboth 4073 1 ((𝐴𝐶𝐵𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  ifcif 4035
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-if 4036
This theorem is referenced by:  ifcld  4080  ifpr  4179  suppr  8237  infpr  8269  ttukeylem3  9193  canthp1lem2  9331  xrmaxlt  11845  xrltmin  11846  xrmaxle  11847  xrlemin  11848  lemaxle  11859  z2ge  11862  ixxin  12019  uzsup  12479  expmulnbnd  12813  discr1  12817  uzin2  13878  rexanre  13880  caubnd  13892  limsupbnd2  14008  rlimcn2  14115  reccn2  14121  lo1mul  14152  rlimno1  14178  fsumsplit  14264  isumless  14362  explecnv  14382  cvgrat  14400  fprodsplit  14481  rpnnen2lem2  14729  sadadd2lem2  14956  sadcaddlem  14963  sadadd2lem  14965  sadadd3  14967  smumullem  14998  pcmpt2  15381  prmreclem4  15407  prmreclem5  15408  prmreclem6  15409  1arith  15415  ressval  15700  acsfn  16089  mplcoe3  19233  mplcoe5  19235  ordtbaslem  20744  pnfnei  20776  mnfnei  20777  uzrest  21453  fclsval  21564  blin  21977  blin2  21985  stdbdxmet  22071  nrginvrcnlem  22238  qtopbaslem  22304  metnrmlem1a  22400  metnrmlem1  22401  addcnlem  22406  evth  22497  xlebnum  22503  minveclem3b  22924  ovolicc1  23008  ismbfd  23130  mbfposr  23142  mbfi1fseqlem4  23208  mbfi1fseqlem5  23209  mbfi1flimlem  23212  itg2const  23230  itg2const2  23231  itg2splitlem  23238  itg2monolem3  23242  itg2gt0  23250  itg2cnlem1  23251  itg2cnlem2  23252  itg2cn  23253  iblre  23283  itgreval  23286  itgneg  23293  iblss  23294  itgitg1  23298  itgle  23299  itgeqa  23303  itgss3  23304  itgless  23306  iblconst  23307  itgconst  23308  ibladdlem  23309  itgaddlem2  23313  iblabslem  23317  iblabsr  23319  iblmulc2  23320  itgmulc2lem2  23322  itgsplit  23325  dveflem  23463  elply2  23673  ply1term  23681  plyeq0lem  23687  plypf1  23689  coe1termlem  23735  coe1term  23736  aalioulem5  23812  aalioulem6  23813  cxpcn3lem  24205  o1cxp  24418  cxp2lim  24420  cxploglim  24421  cxploglim2  24422  ftalem1  24516  ftalem2  24517  ftalem4  24519  muf  24583  chtdif  24601  ppidif  24606  prmorcht  24621  muinv  24636  chtppilim  24881  rplogsumlem2  24891  dchrvmasumiflem1  24907  dchrvmasumiflem2  24908  rpvmasum2  24918  rplogsum  24933  ostth2lem2  25040  ostth2lem3  25041  ostth2lem4  25042  eupath2  26273  resvval  28964  signspval  29761  signswmnd  29766  mblfinlem2  32413  mbfposadd  32423  cnambfre  32424  itg2addnclem  32427  itg2addnc  32430  itg2gt0cn  32431  ibladdnclem  32432  itgaddnclem2  32435  iblabsnclem  32439  iblmulc2nc  32441  itgmulc2nclem2  32443  bddiblnc  32446  ftc1anclem5  32455  ftc1anclem7  32457  ftc1anclem8  32458  areaquad  36617  mullimc  38480  mullimcf  38487  addlimc  38512  limclner  38515  stoweidlem5  38695  eupth2lems  41401  linc0scn0  42001  linc1  42003
  Copyright terms: Public domain W3C validator