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

Theorem ifcl 3614
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 2356 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2356 . 2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( B  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
31, 2ifboth 3609 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 1696   ifcif 3578
This theorem is referenced by:  ifpr  3694  soltmin  5098  pw2f1olem  6982  unxpdomlem3  7085  suppr  7235  wemaplem2  7278  cantnfp1lem1  7396  cantnfp1lem2  7397  cantnfp1lem3  7398  cantnflem1d  7406  cantnflem1  7407  ttukeylem3  8154  canthp1lem2  8291  xrmaxlt  10526  xrltmin  10527  xrmaxle  10528  xrlemin  10529  z2ge  10541  ixxin  10689  uzsup  10983  expmulnbnd  11249  discr1  11253  uzin2  11844  rexanre  11846  rexuzre  11852  rexico  11853  caubnd  11858  limsupgre  11971  limsupbnd2  11973  rlim3  11988  o1lo1  12027  rlimclim1  12035  lo1resb  12054  o1resb  12056  rlimcn2  12080  reccn2  12086  o1of2  12102  o1rlimmul  12108  lo1mul  12117  lo1le  12141  rlimno1  12143  fsumsplit  12228  isumless  12320  explecnv  12339  cvgrat  12355  rpnnen2lem2  12510  ruclem1  12525  ruclem10  12533  bitsfzo  12642  sadadd2lem2  12657  sadcaddlem  12664  sadadd2lem  12666  sadadd3  12668  smumullem  12699  pcmpt2  12957  prmreclem4  12982  prmreclem5  12983  prmreclem6  12984  1arith  12990  ramub1lem2  13090  ramcl  13092  ressval  13211  wunress  13223  acsfn  13577  frgpuptf  15095  gsumzsplit  15222  psr1cl  16163  subrgpsr  16179  mvrf  16185  mplmon  16223  mplmonmul  16224  mplcoe1  16225  mplcoe3  16226  mplcoe2  16227  coe1tmfv2  16367  xrsds  16430  ordtbaslem  16934  pnfnei  16966  mnfnei  16967  xkopt  17365  uzrest  17608  fclsval  17719  tsmssplit  17850  blin  17986  ssblex  17990  blin2  17991  stdbdxmet  18077  stdbdmet  18078  stdbdbl  18079  stdbdmopn  18080  nlmvscnlem1  18213  nrginvrcnlem  18217  qtopbaslem  18283  tgioo  18318  xrsxmet  18331  icccmplem2  18344  metnrmlem1a  18378  metnrmlem1  18379  addcnlem  18384  evth  18473  xlebnum  18479  ipcnlem1  18688  minveclem3b  18808  ivthlem2  18828  ovolicc1  18891  ovolicc2lem5  18896  ioombl1lem1  18931  ioombl1lem3  18933  ioombl1lem4  18934  ismbfd  19011  mbfmax  19020  mbfposr  19023  i1fres  19076  itg1climres  19085  mbfi1fseqlem3  19088  mbfi1fseqlem4  19089  mbfi1fseqlem5  19090  mbfi1flimlem  19093  itg2const  19111  itg2const2  19112  itg2splitlem  19119  itg2monolem3  19123  itg2gt0  19131  itg2cnlem1  19132  itg2cnlem2  19133  itg2cn  19134  iblre  19164  itgreval  19167  itgneg  19174  iblss  19175  itgitg1  19179  itgle  19180  itgeqa  19184  itgss3  19185  itgless  19187  iblconst  19188  itgconst  19189  ibladdlem  19190  itgaddlem2  19194  iblabslem  19198  iblabsr  19200  iblmulc2  19201  itgmulc2lem2  19203  itgsplit  19206  limcres  19252  dveflem  19342  dvferm1lem  19347  dvferm2lem  19349  dvlip2  19358  lhop1  19377  dvfsumrlim  19394  evlslem3  19414  evlslem1  19415  mdegaddle  19476  deg1addle2  19504  deg1sublt  19512  ply1divmo  19537  elply2  19594  ply1term  19602  plyeq0lem  19608  plypf1  19610  plyaddlem1  19611  plyaddlem  19613  coeaddlem  19646  coe1termlem  19655  coe1term  19656  dgradd2  19665  plydiveu  19694  aalioulem5  19732  aalioulem6  19733  abelthlem9  19832  logcnlem2  20006  logcnlem3  20007  cxpcn3lem  20103  o1cxp  20285  cxp2lim  20287  cxploglim  20288  cxploglim2  20289  ftalem1  20326  ftalem2  20327  ftalem4  20329  muf  20394  chtdif  20412  ppidif  20417  prmorcht  20432  muinv  20449  chebbnd1lem1  20634  chtppilim  20640  rplogsumlem2  20650  dchrisumlem3  20656  dchrvmasumiflem1  20666  dchrvmasumiflem2  20667  rpvmasum2  20677  rplogsum  20692  ostth2lem2  20799  ostth2lem3  20800  ostth2lem4  20801  ostth3  20803  dstfrvunirn  23690  indispcon  23780  eupath2  23919  itg2addnclem  25003  itg2addnclem2  25004  itg2addnc  25005  itg2gt0cn  25006  ibladdnclem  25007  itgaddnclem2  25010  iblabsnclem  25014  iblmulc2nc  25016  itgmulc2nclem2  25018  bddiblnc  25021  irrapxlem4  27013  irrapxlem5  27014  kelac1  27264  uvcvvcl2  27340  uvcff  27343  mamudiagcl  27560  refsum2cnlem1  27811  stoweidlem5  27857  stoweid  27915
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-if 3579
  Copyright terms: Public domain W3C validator