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

Theorem ifcl 4163
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 2718 . 2 (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝐴𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
2 eleq1 2718 . 2 (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝐵𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
31, 2ifboth 4157 1 ((𝐴𝐶𝐵𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  ifcif 4119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-if 4120
This theorem is referenced by:  ifcld  4164  ifpr  4265  suppr  8418  infpr  8450  ttukeylem3  9371  canthp1lem2  9513  xrmaxlt  12050  xrltmin  12051  xrmaxle  12052  xrlemin  12053  lemaxle  12064  z2ge  12067  ixxin  12230  uzsup  12702  expmulnbnd  13036  discr1  13040  uzin2  14128  rexanre  14130  caubnd  14142  limsupbnd2  14258  rlimcn2  14365  reccn2  14371  lo1mul  14402  rlimno1  14428  fsumsplit  14515  isumless  14621  explecnv  14641  cvgrat  14659  fprodsplit  14740  rpnnen2lem2  14988  sadadd2lem2  15219  sadcaddlem  15226  sadadd2lem  15228  sadadd3  15230  smumullem  15261  pcmpt2  15644  prmreclem4  15670  prmreclem5  15671  prmreclem6  15672  1arith  15678  ressval  15974  acsfn  16367  mplcoe3  19514  mplcoe5  19516  ordtbaslem  21040  pnfnei  21072  mnfnei  21073  uzrest  21748  fclsval  21859  blin  22273  blin2  22281  stdbdxmet  22367  nrginvrcnlem  22542  qtopbaslem  22609  metnrmlem1a  22708  metnrmlem1  22709  addcnlem  22714  evth  22805  xlebnum  22811  minveclem3b  23245  ovolicc1  23330  ismbfd  23452  mbfposr  23464  mbfi1fseqlem4  23530  mbfi1fseqlem5  23531  mbfi1flimlem  23534  itg2const  23552  itg2const2  23553  itg2splitlem  23560  itg2monolem3  23564  itg2gt0  23572  itg2cnlem1  23573  itg2cnlem2  23574  itg2cn  23575  iblre  23605  itgreval  23608  itgneg  23615  iblss  23616  itgitg1  23620  itgle  23621  itgeqa  23625  itgss3  23626  itgless  23628  iblconst  23629  itgconst  23630  ibladdlem  23631  itgaddlem2  23635  iblabslem  23639  iblabsr  23641  iblmulc2  23642  itgmulc2lem2  23644  itgsplit  23647  dveflem  23787  elply2  23997  ply1term  24005  plyeq0lem  24011  plypf1  24013  coe1termlem  24059  coe1term  24060  aalioulem5  24136  aalioulem6  24137  cxpcn3lem  24533  o1cxp  24746  cxp2lim  24748  cxploglim  24749  cxploglim2  24750  ftalem1  24844  ftalem2  24845  ftalem4  24847  muf  24911  chtdif  24929  ppidif  24934  prmorcht  24949  muinv  24964  chtppilim  25209  rplogsumlem2  25219  dchrvmasumiflem1  25235  dchrvmasumiflem2  25236  rpvmasum2  25246  rplogsum  25261  ostth2lem2  25368  ostth2lem3  25369  ostth2lem4  25370  eupth2lems  27216  resvval  29955  signspval  30757  signswmnd  30762  mblfinlem2  33577  mbfposadd  33587  cnambfre  33588  itg2addnclem  33591  itg2addnc  33594  itg2gt0cn  33595  ibladdnclem  33596  itgaddnclem2  33599  iblabsnclem  33603  iblmulc2nc  33605  itgmulc2nclem2  33607  bddiblnc  33610  ftc1anclem5  33619  ftc1anclem7  33621  ftc1anclem8  33622  areaquad  38119  mullimc  40166  mullimcf  40173  addlimc  40198  limclner  40201  stoweidlem5  40540  linc0scn0  42537  linc1  42539
  Copyright terms: Public domain W3C validator