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

Theorem ifcl 3836
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 2503 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2503 . 2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( B  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
31, 2ifboth 3830 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 1756   ifcif 3796
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-if 3797
This theorem is referenced by:  ifcld  3837  ifpr  3929  soltmin  5242  pw2f1olem  7420  unxpdomlem3  7524  suppr  7723  wemaplem2  7766  cantnfp1lem1OLD  7917  cantnfp1lem2OLD  7918  cantnfp1lem3OLD  7919  cantnflem1dOLD  7924  cantnflem1OLD  7925  ttukeylem3  8685  canthp1lem2  8825  xrmaxlt  11158  xrltmin  11159  xrmaxle  11160  xrlemin  11161  z2ge  11173  ixxin  11322  uzsup  11707  expmulnbnd  12001  discr1  12005  uzin2  12837  rexanre  12839  rexuzre  12845  rexico  12846  caubnd  12851  limsupgre  12964  limsupbnd2  12966  rlim3  12981  o1lo1  13020  rlimclim1  13028  lo1resb  13047  o1resb  13049  rlimcn2  13073  reccn2  13079  o1of2  13095  o1rlimmul  13101  lo1mul  13110  lo1le  13134  rlimno1  13136  fsumsplit  13221  isumless  13313  explecnv  13332  cvgrat  13348  rpnnen2lem2  13503  ruclem1  13518  ruclem10  13526  bitsfzo  13636  sadadd2lem2  13651  sadcaddlem  13658  sadadd2lem  13660  sadadd3  13662  smumullem  13693  pcmpt2  13960  prmreclem4  13985  prmreclem5  13986  prmreclem6  13987  1arith  13993  ramub1lem2  14093  ramcl  14095  ressval  14230  wunress  14242  acsfn  14602  frgpuptf  16272  gsumzsplitOLD  16424  psr1cl  17478  subrgpsr  17496  mvrf  17502  mplcoe3  17550  mplcoe3OLD  17551  mplcoe5  17553  mplcoe2OLD  17555  coe1tmfv2  17733  xrsds  17861  uvcvvcl2  18218  mamudiagcl  18307  maduf  18452  ordtbaslem  18797  pnfnei  18829  mnfnei  18830  xkopt  19233  uzrest  19475  fclsval  19586  blin  20001  ssblex  20008  blin2  20009  stdbdxmet  20095  stdbdmet  20096  stdbdbl  20097  stdbdmopn  20098  nlmvscnlem1  20272  nrginvrcnlem  20276  qtopbaslem  20342  tgioo  20378  xrsxmet  20391  icccmplem2  20405  metnrmlem1a  20439  metnrmlem1  20440  addcnlem  20445  evth  20536  xlebnum  20542  ipcnlem1  20762  minveclem3b  20920  ivthlem2  20941  ovolicc1  21004  ovolicc2lem5  21009  ioombl1lem1  21044  ioombl1lem3  21046  ioombl1lem4  21047  ismbfd  21123  mbfmax  21132  mbfposr  21135  i1fres  21188  itg1climres  21197  mbfi1fseqlem3  21200  mbfi1fseqlem4  21201  mbfi1fseqlem5  21202  mbfi1flimlem  21205  itg2const  21223  itg2const2  21224  itg2splitlem  21231  itg2monolem3  21235  itg2gt0  21243  itg2cnlem1  21244  itg2cnlem2  21245  itg2cn  21246  iblre  21276  itgreval  21279  itgneg  21286  iblss  21287  itgitg1  21291  itgle  21292  itgeqa  21296  itgss3  21297  itgless  21299  iblconst  21300  itgconst  21301  ibladdlem  21302  itgaddlem2  21306  iblabslem  21310  iblabsr  21312  iblmulc2  21313  itgmulc2lem2  21315  itgsplit  21318  limcres  21366  dveflem  21456  dvferm1lem  21461  dvferm2lem  21463  dvlip2  21472  lhop1  21491  dvfsumrlim  21508  mdegaddle  21550  deg1addle2  21579  deg1sublt  21587  ply1divmo  21612  elply2  21669  ply1term  21677  plyeq0lem  21683  plypf1  21685  plyaddlem1  21686  plyaddlem  21688  coeaddlem  21721  coe1termlem  21730  coe1term  21731  dgradd2  21740  plydiveu  21769  aalioulem5  21807  aalioulem6  21808  abelthlem9  21910  logcnlem2  22093  logcnlem3  22094  cxpcn3lem  22190  o1cxp  22373  cxp2lim  22375  cxploglim  22376  cxploglim2  22377  ftalem1  22415  ftalem2  22416  ftalem4  22418  muf  22483  chtdif  22501  ppidif  22506  prmorcht  22521  muinv  22538  chebbnd1lem1  22723  chtppilim  22729  rplogsumlem2  22739  dchrisumlem3  22745  dchrvmasumiflem1  22755  dchrvmasumiflem2  22756  rpvmasum2  22766  rplogsum  22781  ostth2lem2  22888  ostth2lem3  22889  ostth2lem4  22890  ostth3  22892  eupath2  23606  resvval  26300  dstfrvunirn  26862  signspval  26958  lgamgulmlem4  27023  lgamgulmlem6  27025  indispcon  27128  fprodsplit  27481  mblfinlem2  28434  mbfposadd  28444  cnambfre  28445  itg2addnclem  28448  itg2addnclem2  28449  itg2addnclem3  28450  itg2addnc  28451  itg2gt0cn  28452  ibladdnclem  28453  itgaddnclem2  28456  iblabsnclem  28460  iblmulc2nc  28462  itgmulc2nclem2  28464  bddiblnc  28467  ftc1anclem5  28476  ftc1anclem7  28478  ftc1anclem8  28479  irrapxlem4  29171  irrapxlem5  29172  kelac1  29421  areaquad  29597  refsum2cnlem1  29764  stoweidlem5  29805  linc0scn0  30962  linc1  30964
  Copyright terms: Public domain W3C validator