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

Theorem ifcl 3819
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 2493 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2493 . 2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( B  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
31, 2ifboth 3813 1  |-  ( ( A  e.  C  /\  B  e.  C )  ->  if ( ph ,  A ,  B )  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1755   ifcif 3779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-if 3780
This theorem is referenced by:  ifcld  3820  ifpr  3912  soltmin  5225  pw2f1olem  7403  unxpdomlem3  7507  suppr  7706  wemaplem2  7749  cantnfp1lem1OLD  7900  cantnfp1lem2OLD  7901  cantnfp1lem3OLD  7902  cantnflem1dOLD  7907  cantnflem1OLD  7908  ttukeylem3  8668  canthp1lem2  8807  xrmaxlt  11140  xrltmin  11141  xrmaxle  11142  xrlemin  11143  z2ge  11155  ixxin  11304  uzsup  11685  expmulnbnd  11979  discr1  11983  uzin2  12815  rexanre  12817  rexuzre  12823  rexico  12824  caubnd  12829  limsupgre  12942  limsupbnd2  12944  rlim3  12959  o1lo1  12998  rlimclim1  13006  lo1resb  13025  o1resb  13027  rlimcn2  13051  reccn2  13057  o1of2  13073  o1rlimmul  13079  lo1mul  13088  lo1le  13112  rlimno1  13114  fsumsplit  13199  isumless  13290  explecnv  13309  cvgrat  13325  rpnnen2lem2  13480  ruclem1  13495  ruclem10  13503  bitsfzo  13613  sadadd2lem2  13628  sadcaddlem  13635  sadadd2lem  13637  sadadd3  13639  smumullem  13670  pcmpt2  13937  prmreclem4  13962  prmreclem5  13963  prmreclem6  13964  1arith  13970  ramub1lem2  14070  ramcl  14072  ressval  14207  wunress  14219  acsfn  14579  frgpuptf  16246  gsumzsplitOLD  16398  psr1cl  17406  subrgpsr  17424  mvrf  17430  mplcoe3  17478  mplcoe3OLD  17479  mplcoe2  17480  mplcoe2OLD  17481  coe1tmfv2  17625  xrsds  17699  uvcvvcl2  18054  mamudiagcl  18143  maduf  18288  ordtbaslem  18633  pnfnei  18665  mnfnei  18666  xkopt  19069  uzrest  19311  fclsval  19422  blin  19837  ssblex  19844  blin2  19845  stdbdxmet  19931  stdbdmet  19932  stdbdbl  19933  stdbdmopn  19934  nlmvscnlem1  20108  nrginvrcnlem  20112  qtopbaslem  20178  tgioo  20214  xrsxmet  20227  icccmplem2  20241  metnrmlem1a  20275  metnrmlem1  20276  addcnlem  20281  evth  20372  xlebnum  20378  ipcnlem1  20598  minveclem3b  20756  ivthlem2  20777  ovolicc1  20840  ovolicc2lem5  20845  ioombl1lem1  20880  ioombl1lem3  20882  ioombl1lem4  20883  ismbfd  20959  mbfmax  20968  mbfposr  20971  i1fres  21024  itg1climres  21033  mbfi1fseqlem3  21036  mbfi1fseqlem4  21037  mbfi1fseqlem5  21038  mbfi1flimlem  21041  itg2const  21059  itg2const2  21060  itg2splitlem  21067  itg2monolem3  21071  itg2gt0  21079  itg2cnlem1  21080  itg2cnlem2  21081  itg2cn  21082  iblre  21112  itgreval  21115  itgneg  21122  iblss  21123  itgitg1  21127  itgle  21128  itgeqa  21132  itgss3  21133  itgless  21135  iblconst  21136  itgconst  21137  ibladdlem  21138  itgaddlem2  21142  iblabslem  21146  iblabsr  21148  iblmulc2  21149  itgmulc2lem2  21151  itgsplit  21154  limcres  21202  dveflem  21292  dvferm1lem  21297  dvferm2lem  21299  dvlip2  21308  lhop1  21327  dvfsumrlim  21344  mdegaddle  21429  deg1addle2  21458  deg1sublt  21466  ply1divmo  21491  elply2  21548  ply1term  21556  plyeq0lem  21562  plypf1  21564  plyaddlem1  21565  plyaddlem  21567  coeaddlem  21600  coe1termlem  21609  coe1term  21610  dgradd2  21619  plydiveu  21648  aalioulem5  21686  aalioulem6  21687  abelthlem9  21789  logcnlem2  21972  logcnlem3  21973  cxpcn3lem  22069  o1cxp  22252  cxp2lim  22254  cxploglim  22255  cxploglim2  22256  ftalem1  22294  ftalem2  22295  ftalem4  22297  muf  22362  chtdif  22380  ppidif  22385  prmorcht  22400  muinv  22417  chebbnd1lem1  22602  chtppilim  22608  rplogsumlem2  22618  dchrisumlem3  22624  dchrvmasumiflem1  22634  dchrvmasumiflem2  22635  rpvmasum2  22645  rplogsum  22660  ostth2lem2  22767  ostth2lem3  22768  ostth2lem4  22769  ostth3  22771  eupath2  23423  resvval  26148  dstfrvunirn  26704  signspval  26800  lgamgulmlem4  26865  lgamgulmlem6  26867  indispcon  26970  fprodsplit  27322  mblfinlem2  28270  mbfposadd  28280  cnambfre  28281  itg2addnclem  28284  itg2addnclem2  28285  itg2addnclem3  28286  itg2addnc  28287  itg2gt0cn  28288  ibladdnclem  28289  itgaddnclem2  28292  iblabsnclem  28296  iblmulc2nc  28298  itgmulc2nclem2  28300  bddiblnc  28303  ftc1anclem5  28312  ftc1anclem7  28314  ftc1anclem8  28315  irrapxlem4  29008  irrapxlem5  29009  kelac1  29258  areaquad  29434  refsum2cnlem1  29601  stoweidlem5  29643  stoweid  29701  linc0scn0  30663  linc1  30665
  Copyright terms: Public domain W3C validator