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

Theorem ifcl 3735
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 2464 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2464 . 2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( B  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
31, 2ifboth 3730 1  |-  ( ( A  e.  C  /\  B  e.  C )  ->  if ( ph ,  A ,  B )  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   ifcif 3699
This theorem is referenced by:  ifpr  3816  soltmin  5232  pw2f1olem  7171  unxpdomlem3  7274  suppr  7429  wemaplem2  7472  cantnfp1lem1  7590  cantnfp1lem2  7591  cantnfp1lem3  7592  cantnflem1d  7600  cantnflem1  7601  ttukeylem3  8347  canthp1lem2  8484  xrmaxlt  10725  xrltmin  10726  xrmaxle  10727  xrlemin  10728  z2ge  10740  ixxin  10889  uzsup  11199  expmulnbnd  11466  discr1  11470  uzin2  12103  rexanre  12105  rexuzre  12111  rexico  12112  caubnd  12117  limsupgre  12230  limsupbnd2  12232  rlim3  12247  o1lo1  12286  rlimclim1  12294  lo1resb  12313  o1resb  12315  rlimcn2  12339  reccn2  12345  o1of2  12361  o1rlimmul  12367  lo1mul  12376  lo1le  12400  rlimno1  12402  fsumsplit  12488  isumless  12580  explecnv  12599  cvgrat  12615  rpnnen2lem2  12770  ruclem1  12785  ruclem10  12793  bitsfzo  12902  sadadd2lem2  12917  sadcaddlem  12924  sadadd2lem  12926  sadadd3  12928  smumullem  12959  pcmpt2  13217  prmreclem4  13242  prmreclem5  13243  prmreclem6  13244  1arith  13250  ramub1lem2  13350  ramcl  13352  ressval  13471  wunress  13483  acsfn  13839  frgpuptf  15357  gsumzsplit  15484  psr1cl  16421  subrgpsr  16437  mvrf  16443  mplmon  16481  mplmonmul  16482  mplcoe1  16483  mplcoe3  16484  mplcoe2  16485  coe1tmfv2  16622  xrsds  16696  ordtbaslem  17206  pnfnei  17238  mnfnei  17239  xkopt  17640  uzrest  17882  fclsval  17993  tsmssplit  18134  blin  18404  ssblex  18411  blin2  18412  stdbdxmet  18498  stdbdmet  18499  stdbdbl  18500  stdbdmopn  18501  nlmvscnlem1  18675  nrginvrcnlem  18679  qtopbaslem  18745  tgioo  18780  xrsxmet  18793  icccmplem2  18807  metnrmlem1a  18841  metnrmlem1  18842  addcnlem  18847  evth  18937  xlebnum  18943  ipcnlem1  19152  minveclem3b  19282  ivthlem2  19302  ovolicc1  19365  ovolicc2lem5  19370  ioombl1lem1  19405  ioombl1lem3  19407  ioombl1lem4  19408  ismbfd  19485  mbfmax  19494  mbfposr  19497  i1fres  19550  itg1climres  19559  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  mbfi1fseqlem5  19564  mbfi1flimlem  19567  itg2const  19585  itg2const2  19586  itg2splitlem  19593  itg2monolem3  19597  itg2gt0  19605  itg2cnlem1  19606  itg2cnlem2  19607  itg2cn  19608  iblre  19638  itgreval  19641  itgneg  19648  iblss  19649  itgitg1  19653  itgle  19654  itgeqa  19658  itgss3  19659  itgless  19661  iblconst  19662  itgconst  19663  ibladdlem  19664  itgaddlem2  19668  iblabslem  19672  iblabsr  19674  iblmulc2  19675  itgmulc2lem2  19677  itgsplit  19680  limcres  19726  dveflem  19816  dvferm1lem  19821  dvferm2lem  19823  dvlip2  19832  lhop1  19851  dvfsumrlim  19868  evlslem3  19888  evlslem1  19889  mdegaddle  19950  deg1addle2  19978  deg1sublt  19986  ply1divmo  20011  elply2  20068  ply1term  20076  plyeq0lem  20082  plypf1  20084  plyaddlem1  20085  plyaddlem  20087  coeaddlem  20120  coe1termlem  20129  coe1term  20130  dgradd2  20139  plydiveu  20168  aalioulem5  20206  aalioulem6  20207  abelthlem9  20309  logcnlem2  20487  logcnlem3  20488  cxpcn3lem  20584  o1cxp  20766  cxp2lim  20768  cxploglim  20769  cxploglim2  20770  ftalem1  20808  ftalem2  20809  ftalem4  20811  muf  20876  chtdif  20894  ppidif  20899  prmorcht  20914  muinv  20931  chebbnd1lem1  21116  chtppilim  21122  rplogsumlem2  21132  dchrisumlem3  21138  dchrvmasumiflem1  21148  dchrvmasumiflem2  21149  rpvmasum2  21159  rplogsum  21174  ostth2lem2  21281  ostth2lem3  21282  ostth2lem4  21283  ostth3  21285  eupath2  21655  dstfrvunirn  24685  lgamgulmlem4  24769  lgamgulmlem6  24771  indispcon  24874  fprodsplit  25242  mblfinlem  26143  mbfposadd  26153  cnambfre  26154  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  itg2addnc  26158  itg2gt0cn  26159  ibladdnclem  26160  itgaddnclem2  26163  iblabsnclem  26167  iblmulc2nc  26169  itgmulc2nclem2  26171  bddiblnc  26174  irrapxlem4  26778  irrapxlem5  26779  kelac1  27029  uvcvvcl2  27105  uvcff  27108  mamudiagcl  27325  refsum2cnlem1  27575  stoweidlem5  27621  stoweid  27679
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-if 3700
  Copyright terms: Public domain W3C validator