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

Theorem ifcl 3601
Description: Membership (closure) of a conditional operator. (Contributed by NM, 4-Apr-2005.)
Assertion
Ref Expression
ifcl  |-  ( ( A  e.  C  /\  B  e.  C )  ->  if ( ph ,  A ,  B )  e.  C )

Proof of Theorem ifcl
StepHypRef Expression
1 eleq1 2343 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2343 . 2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( B  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
31, 2ifboth 3596 1  |-  ( ( A  e.  C  /\  B  e.  C )  ->  if ( ph ,  A ,  B )  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1684   ifcif 3565
This theorem is referenced by:  ifpr  3681  soltmin  5082  pw2f1olem  6966  unxpdomlem3  7069  suppr  7219  wemaplem2  7262  cantnfp1lem1  7380  cantnfp1lem2  7381  cantnfp1lem3  7382  cantnflem1d  7390  cantnflem1  7391  ttukeylem3  8138  canthp1lem2  8275  xrmaxlt  10510  xrltmin  10511  xrmaxle  10512  xrlemin  10513  z2ge  10525  ixxin  10673  uzsup  10967  expmulnbnd  11233  discr1  11237  uzin2  11828  rexanre  11830  rexuzre  11836  rexico  11837  caubnd  11842  limsupgre  11955  limsupbnd2  11957  rlim3  11972  o1lo1  12011  rlimclim1  12019  lo1resb  12038  o1resb  12040  rlimcn2  12064  reccn2  12070  o1of2  12086  o1rlimmul  12092  lo1mul  12101  lo1le  12125  rlimno1  12127  fsumsplit  12212  isumless  12304  explecnv  12323  cvgrat  12339  rpnnen2lem2  12494  ruclem1  12509  ruclem10  12517  bitsfzo  12626  sadadd2lem2  12641  sadcaddlem  12648  sadadd2lem  12650  sadadd3  12652  smumullem  12683  pcmpt2  12941  prmreclem4  12966  prmreclem5  12967  prmreclem6  12968  1arith  12974  ramub1lem2  13074  ramcl  13076  ressval  13195  wunress  13207  acsfn  13561  frgpuptf  15079  gsumzsplit  15206  psr1cl  16147  subrgpsr  16163  mvrf  16169  mplmon  16207  mplmonmul  16208  mplcoe1  16209  mplcoe3  16210  mplcoe2  16211  coe1tmfv2  16351  xrsds  16414  ordtbaslem  16918  pnfnei  16950  mnfnei  16951  xkopt  17349  uzrest  17592  fclsval  17703  tsmssplit  17834  blin  17970  ssblex  17974  blin2  17975  stdbdxmet  18061  stdbdmet  18062  stdbdbl  18063  stdbdmopn  18064  nlmvscnlem1  18197  nrginvrcnlem  18201  qtopbaslem  18267  tgioo  18302  xrsxmet  18315  icccmplem2  18328  metnrmlem1a  18362  metnrmlem1  18363  addcnlem  18368  evth  18457  xlebnum  18463  ipcnlem1  18672  minveclem3b  18792  ivthlem2  18812  ovolicc1  18875  ovolicc2lem5  18880  ioombl1lem1  18915  ioombl1lem3  18917  ioombl1lem4  18918  ismbfd  18995  mbfmax  19004  mbfposr  19007  i1fres  19060  itg1climres  19069  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  mbfi1fseqlem5  19074  mbfi1flimlem  19077  itg2const  19095  itg2const2  19096  itg2splitlem  19103  itg2monolem3  19107  itg2gt0  19115  itg2cnlem1  19116  itg2cnlem2  19117  itg2cn  19118  iblre  19148  itgreval  19151  itgneg  19158  iblss  19159  itgitg1  19163  itgle  19164  itgeqa  19168  itgss3  19169  itgless  19171  iblconst  19172  itgconst  19173  ibladdlem  19174  itgaddlem2  19178  iblabslem  19182  iblabsr  19184  iblmulc2  19185  itgmulc2lem2  19187  itgsplit  19190  limcres  19236  dveflem  19326  dvferm1lem  19331  dvferm2lem  19333  dvlip2  19342  lhop1  19361  dvfsumrlim  19378  evlslem3  19398  evlslem1  19399  mdegaddle  19460  deg1addle2  19488  deg1sublt  19496  ply1divmo  19521  elply2  19578  ply1term  19586  plyeq0lem  19592  plypf1  19594  plyaddlem1  19595  plyaddlem  19597  coeaddlem  19630  coe1termlem  19639  coe1term  19640  dgradd2  19649  plydiveu  19678  aalioulem5  19716  aalioulem6  19717  abelthlem9  19816  logcnlem2  19990  logcnlem3  19991  cxpcn3lem  20087  o1cxp  20269  cxp2lim  20271  cxploglim  20272  cxploglim2  20273  ftalem1  20310  ftalem2  20311  ftalem4  20313  muf  20378  chtdif  20396  ppidif  20401  prmorcht  20416  muinv  20433  chebbnd1lem1  20618  chtppilim  20624  rplogsumlem2  20634  dchrisumlem3  20640  dchrvmasumiflem1  20650  dchrvmasumiflem2  20651  rpvmasum2  20661  rplogsum  20676  ostth2lem2  20783  ostth2lem3  20784  ostth2lem4  20785  ostth3  20787  dstfrvunirn  23675  indispcon  23765  eupath2  23904  irrapxlem4  26910  irrapxlem5  26911  kelac1  27161  uvcvvcl2  27237  uvcff  27240  mamudiagcl  27457  refsum2cnlem1  27708  stoweidlem5  27754  stoweid  27812
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-if 3566
  Copyright terms: Public domain W3C validator