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

Theorem ifcl 3777
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 2498 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2498 . 2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( B  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
31, 2ifboth 3772 1  |-  ( ( A  e.  C  /\  B  e.  C )  ->  if ( ph ,  A ,  B )  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    e. wcel 1726   ifcif 3741
This theorem is referenced by:  ifpr  3858  soltmin  5275  pw2f1olem  7214  unxpdomlem3  7317  suppr  7475  wemaplem2  7518  cantnfp1lem1  7636  cantnfp1lem2  7637  cantnfp1lem3  7638  cantnflem1d  7646  cantnflem1  7647  ttukeylem3  8393  canthp1lem2  8530  xrmaxlt  10771  xrltmin  10772  xrmaxle  10773  xrlemin  10774  z2ge  10786  ixxin  10935  uzsup  11246  expmulnbnd  11513  discr1  11517  uzin2  12150  rexanre  12152  rexuzre  12158  rexico  12159  caubnd  12164  limsupgre  12277  limsupbnd2  12279  rlim3  12294  o1lo1  12333  rlimclim1  12341  lo1resb  12360  o1resb  12362  rlimcn2  12386  reccn2  12392  o1of2  12408  o1rlimmul  12414  lo1mul  12423  lo1le  12447  rlimno1  12449  fsumsplit  12535  isumless  12627  explecnv  12646  cvgrat  12662  rpnnen2lem2  12817  ruclem1  12832  ruclem10  12840  bitsfzo  12949  sadadd2lem2  12964  sadcaddlem  12971  sadadd2lem  12973  sadadd3  12975  smumullem  13006  pcmpt2  13264  prmreclem4  13289  prmreclem5  13290  prmreclem6  13291  1arith  13297  ramub1lem2  13397  ramcl  13399  ressval  13518  wunress  13530  acsfn  13886  frgpuptf  15404  gsumzsplit  15531  psr1cl  16468  subrgpsr  16484  mvrf  16490  mplmon  16528  mplmonmul  16529  mplcoe1  16530  mplcoe3  16531  mplcoe2  16532  coe1tmfv2  16669  xrsds  16743  ordtbaslem  17254  pnfnei  17286  mnfnei  17287  xkopt  17689  uzrest  17931  fclsval  18042  tsmssplit  18183  blin  18453  ssblex  18460  blin2  18461  stdbdxmet  18547  stdbdmet  18548  stdbdbl  18549  stdbdmopn  18550  nlmvscnlem1  18724  nrginvrcnlem  18728  qtopbaslem  18794  tgioo  18829  xrsxmet  18842  icccmplem2  18856  metnrmlem1a  18890  metnrmlem1  18891  addcnlem  18896  evth  18986  xlebnum  18992  ipcnlem1  19201  minveclem3b  19331  ivthlem2  19351  ovolicc1  19414  ovolicc2lem5  19419  ioombl1lem1  19454  ioombl1lem3  19456  ioombl1lem4  19457  ismbfd  19534  mbfmax  19543  mbfposr  19546  i1fres  19599  itg1climres  19608  mbfi1fseqlem3  19611  mbfi1fseqlem4  19612  mbfi1fseqlem5  19613  mbfi1flimlem  19616  itg2const  19634  itg2const2  19635  itg2splitlem  19642  itg2monolem3  19646  itg2gt0  19654  itg2cnlem1  19655  itg2cnlem2  19656  itg2cn  19657  iblre  19687  itgreval  19690  itgneg  19697  iblss  19698  itgitg1  19702  itgle  19703  itgeqa  19707  itgss3  19708  itgless  19710  iblconst  19711  itgconst  19712  ibladdlem  19713  itgaddlem2  19717  iblabslem  19721  iblabsr  19723  iblmulc2  19724  itgmulc2lem2  19726  itgsplit  19729  limcres  19775  dveflem  19865  dvferm1lem  19870  dvferm2lem  19872  dvlip2  19881  lhop1  19900  dvfsumrlim  19917  evlslem3  19937  evlslem1  19938  mdegaddle  19999  deg1addle2  20027  deg1sublt  20035  ply1divmo  20060  elply2  20117  ply1term  20125  plyeq0lem  20131  plypf1  20133  plyaddlem1  20134  plyaddlem  20136  coeaddlem  20169  coe1termlem  20178  coe1term  20179  dgradd2  20188  plydiveu  20217  aalioulem5  20255  aalioulem6  20256  abelthlem9  20358  logcnlem2  20536  logcnlem3  20537  cxpcn3lem  20633  o1cxp  20815  cxp2lim  20817  cxploglim  20818  cxploglim2  20819  ftalem1  20857  ftalem2  20858  ftalem4  20860  muf  20925  chtdif  20943  ppidif  20948  prmorcht  20963  muinv  20980  chebbnd1lem1  21165  chtppilim  21171  rplogsumlem2  21181  dchrisumlem3  21187  dchrvmasumiflem1  21197  dchrvmasumiflem2  21198  rpvmasum2  21208  rplogsum  21223  ostth2lem2  21330  ostth2lem3  21331  ostth2lem4  21332  ostth3  21334  eupath2  21704  dstfrvunirn  24734  lgamgulmlem4  24818  lgamgulmlem6  24820  indispcon  24923  fprodsplit  25291  mblfinlem2  26246  mbfposadd  26256  cnambfre  26257  itg2addnclem  26258  itg2addnclem2  26259  itg2addnclem3  26260  itg2addnc  26261  itg2gt0cn  26262  ibladdnclem  26263  itgaddnclem2  26266  iblabsnclem  26270  iblmulc2nc  26272  itgmulc2nclem2  26274  bddiblnc  26277  ftc1anclem5  26286  ftc1anclem7  26288  ftc1anclem8  26289  irrapxlem4  26890  irrapxlem5  26891  kelac1  27140  uvcvvcl2  27216  uvcff  27219  mamudiagcl  27436  refsum2cnlem1  27686  stoweidlem5  27732  stoweid  27790
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-if 3742
  Copyright terms: Public domain W3C validator