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

Theorem ifcl 3981
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 2539 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2539 . 2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( B  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
31, 2ifboth 3975 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 1767   ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940
This theorem is referenced by:  ifcld  3982  ifpr  4075  soltmin  5404  pw2f1olem  7618  unxpdomlem3  7723  suppr  7925  wemaplem2  7968  cantnfp1lem1OLD  8119  cantnfp1lem2OLD  8120  cantnfp1lem3OLD  8121  cantnflem1dOLD  8126  cantnflem1OLD  8127  ttukeylem3  8887  canthp1lem2  9027  xrmaxlt  11378  xrltmin  11379  xrmaxle  11380  xrlemin  11381  z2ge  11393  ixxin  11542  uzsup  11954  expmulnbnd  12262  discr1  12266  uzin2  13136  rexanre  13138  rexuzre  13144  rexico  13145  caubnd  13150  limsupgre  13263  limsupbnd2  13265  rlim3  13280  o1lo1  13319  rlimclim1  13327  lo1resb  13346  o1resb  13348  rlimcn2  13372  reccn2  13378  o1of2  13394  o1rlimmul  13400  lo1mul  13409  lo1le  13433  rlimno1  13435  fsumsplit  13521  isumless  13616  explecnv  13635  cvgrat  13651  rpnnen2lem2  13806  ruclem1  13821  ruclem10  13829  bitsfzo  13940  sadadd2lem2  13955  sadcaddlem  13962  sadadd2lem  13964  sadadd3  13966  smumullem  13997  pcmpt2  14267  prmreclem4  14292  prmreclem5  14293  prmreclem6  14294  1arith  14300  ramub1lem2  14400  ramcl  14402  ressval  14538  wunress  14550  acsfn  14910  frgpuptf  16584  gsumzsplitOLD  16736  psr1cl  17826  subrgpsr  17845  mvrf  17851  mplcoe3  17899  mplcoe3OLD  17900  mplcoe5  17902  mplcoe2OLD  17904  coe1tmfv2  18087  xrsds  18229  uvcvvcl2  18586  mamumat1cl  18708  maduf  18910  ordtbaslem  19455  pnfnei  19487  mnfnei  19488  xkopt  19891  uzrest  20133  fclsval  20244  blin  20659  ssblex  20666  blin2  20667  stdbdxmet  20753  stdbdmet  20754  stdbdbl  20755  stdbdmopn  20756  nlmvscnlem1  20930  nrginvrcnlem  20934  qtopbaslem  21000  tgioo  21036  xrsxmet  21049  icccmplem2  21063  metnrmlem1a  21097  metnrmlem1  21098  addcnlem  21103  evth  21194  xlebnum  21200  ipcnlem1  21420  minveclem3b  21578  ivthlem2  21599  ovolicc1  21662  ovolicc2lem5  21667  ioombl1lem1  21703  ioombl1lem3  21705  ioombl1lem4  21706  ismbfd  21782  mbfmax  21791  mbfposr  21794  i1fres  21847  itg1climres  21856  mbfi1fseqlem3  21859  mbfi1fseqlem4  21860  mbfi1fseqlem5  21861  mbfi1flimlem  21864  itg2const  21882  itg2const2  21883  itg2splitlem  21890  itg2monolem3  21894  itg2gt0  21902  itg2cnlem1  21903  itg2cnlem2  21904  itg2cn  21905  iblre  21935  itgreval  21938  itgneg  21945  iblss  21946  itgitg1  21950  itgle  21951  itgeqa  21955  itgss3  21956  itgless  21958  iblconst  21959  itgconst  21960  ibladdlem  21961  itgaddlem2  21965  iblabslem  21969  iblabsr  21971  iblmulc2  21972  itgmulc2lem2  21974  itgsplit  21977  limcres  22025  dveflem  22115  dvferm1lem  22120  dvferm2lem  22122  dvlip2  22131  lhop1  22150  dvfsumrlim  22167  mdegaddle  22209  deg1addle2  22238  deg1sublt  22246  ply1divmo  22271  elply2  22328  ply1term  22336  plyeq0lem  22342  plypf1  22344  plyaddlem1  22345  plyaddlem  22347  coeaddlem  22380  coe1termlem  22389  coe1term  22390  dgradd2  22399  plydiveu  22428  aalioulem5  22466  aalioulem6  22467  abelthlem9  22569  logcnlem2  22752  logcnlem3  22753  cxpcn3lem  22849  o1cxp  23032  cxp2lim  23034  cxploglim  23035  cxploglim2  23036  ftalem1  23074  ftalem2  23075  ftalem4  23077  muf  23142  chtdif  23160  ppidif  23165  prmorcht  23180  muinv  23197  chebbnd1lem1  23382  chtppilim  23388  rplogsumlem2  23398  dchrisumlem3  23404  dchrvmasumiflem1  23414  dchrvmasumiflem2  23415  rpvmasum2  23425  rplogsum  23440  ostth2lem2  23547  ostth2lem3  23548  ostth2lem4  23549  ostth3  23551  eupath2  24656  resvval  27480  dstfrvunirn  28053  signspval  28149  lgamgulmlem4  28214  lgamgulmlem6  28216  indispcon  28319  fprodsplit  28672  mblfinlem2  29629  mbfposadd  29639  cnambfre  29640  itg2addnclem  29643  itg2addnclem2  29644  itg2addnclem3  29645  itg2addnc  29646  itg2gt0cn  29647  ibladdnclem  29648  itgaddnclem2  29651  iblabsnclem  29655  iblmulc2nc  29657  itgmulc2nclem2  29659  bddiblnc  29662  ftc1anclem5  29671  ftc1anclem7  29673  ftc1anclem8  29674  irrapxlem4  30365  irrapxlem5  30366  kelac1  30613  areaquad  30789  refsum2cnlem1  30990  mullimc  31158  mullimcf  31165  0ellimcdiv  31191  limclner  31193  icccncfext  31226  cncfiooicclem1  31232  stoweidlem5  31305  sqwvfourb  31530  fouriersw  31532  linc0scn0  32097  linc1  32099
  Copyright terms: Public domain W3C validator