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

Theorem ifcl 3935
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 2528 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2528 . 2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( B  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
31, 2ifboth 3929 1  |-  ( ( A  e.  C  /\  B  e.  C )  ->  if ( ph ,  A ,  B )  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    e. wcel 1898   ifcif 3893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-if 3894
This theorem is referenced by:  ifcld  3936  ifpr  4032  suppr  8013  infpr  8045  ttukeylem3  8967  canthp1lem2  9104  xrmaxlt  11505  xrltmin  11506  xrmaxle  11507  xrlemin  11508  z2ge  11520  ixxin  11681  uzsup  12122  expmulnbnd  12436  discr1  12440  uzin2  13456  rexanre  13458  caubnd  13470  limsupbnd2  13595  limsupbnd2OLD  13596  rlimcn2  13703  reccn2  13709  lo1mul  13740  rlimno1  13766  fsumsplit  13855  isumless  13952  explecnv  13972  cvgrat  13988  fprodsplit  14069  rpnnen2lem2  14317  sadadd2lem2  14473  sadcaddlem  14480  sadadd2lem  14482  sadadd3  14484  smumullem  14515  pcmpt2  14887  prmreclem4  14912  prmreclem5  14913  prmreclem6  14914  1arith  14920  ressval  15225  acsfn  15614  mplcoe3  18739  mplcoe5  18741  ordtbaslem  20253  pnfnei  20285  mnfnei  20286  uzrest  20961  fclsval  21072  blin  21485  blin2  21493  stdbdxmet  21579  nrginvrcnlem  21742  qtopbaslem  21828  metnrmlem1a  21924  metnrmlem1  21925  metnrmlem1aOLD  21939  metnrmlem1OLD  21940  addcnlem  21945  evth  22036  xlebnum  22045  minveclem3b  22419  minveclem3bOLD  22431  ovolicc1  22518  ismbfd  22645  mbfposr  22657  mbfi1fseqlem4  22725  mbfi1fseqlem5  22726  mbfi1flimlem  22729  itg2const  22747  itg2const2  22748  itg2splitlem  22755  itg2monolem3  22759  itg2gt0  22767  itg2cnlem1  22768  itg2cnlem2  22769  itg2cn  22770  iblre  22800  itgreval  22803  itgneg  22810  iblss  22811  itgitg1  22815  itgle  22816  itgeqa  22820  itgss3  22821  itgless  22823  iblconst  22824  itgconst  22825  ibladdlem  22826  itgaddlem2  22830  iblabslem  22834  iblabsr  22836  iblmulc2  22837  itgmulc2lem2  22839  itgsplit  22842  dveflem  22980  elply2  23199  ply1term  23207  plyeq0lem  23213  plypf1  23215  coe1termlem  23261  coe1term  23262  aalioulem5  23341  aalioulem6  23342  cxpcn3lem  23736  o1cxp  23949  cxp2lim  23951  cxploglim  23952  cxploglim2  23953  ftalem1  24046  ftalem2  24047  ftalem4  24049  ftalem4OLD  24051  muf  24116  chtdif  24134  ppidif  24139  prmorcht  24154  muinv  24171  chtppilim  24362  rplogsumlem2  24372  dchrvmasumiflem1  24388  dchrvmasumiflem2  24389  rpvmasum2  24399  rplogsum  24414  ostth2lem2  24521  ostth2lem3  24522  ostth2lem4  24523  eupath2  25757  resvval  28639  signspval  29490  signswmnd  29495  mblfinlem2  32023  mbfposadd  32033  cnambfre  32034  itg2addnclem  32038  itg2addnc  32041  itg2gt0cn  32042  ibladdnclem  32043  itgaddnclem2  32046  iblabsnclem  32050  iblmulc2nc  32052  itgmulc2nclem2  32054  bddiblnc  32057  ftc1anclem5  32066  ftc1anclem7  32068  ftc1anclem8  32069  areaquad  36146  mullimc  37734  mullimcf  37741  addlimc  37767  limclner  37770  stoweidlem5  37903  linc0scn0  40489  linc1  40491
  Copyright terms: Public domain W3C validator