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

Theorem ifcl 3971
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 2526 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2526 . 2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( B  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
31, 2ifboth 3965 1  |-  ( ( A  e.  C  /\  B  e.  C )  ->  if ( ph ,  A ,  B )  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1823   ifcif 3929
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-if 3930
This theorem is referenced by:  ifcld  3972  ifpr  4064  suppr  7921  cantnfp1lem1OLD  8114  cantnfp1lem2OLD  8115  cantnfp1lem3OLD  8116  cantnflem1dOLD  8121  cantnflem1OLD  8122  ttukeylem3  8882  canthp1lem2  9020  xrmaxlt  11385  xrltmin  11386  xrmaxle  11387  xrlemin  11388  z2ge  11400  ixxin  11549  uzsup  11972  expmulnbnd  12280  discr1  12284  uzin2  13259  rexanre  13261  caubnd  13273  limsupbnd2  13388  rlimcn2  13495  reccn2  13501  lo1mul  13532  rlimno1  13558  fsumsplit  13644  isumless  13739  explecnv  13758  cvgrat  13774  fprodsplit  13852  rpnnen2lem2  14033  sadadd2lem2  14184  sadcaddlem  14191  sadadd2lem  14193  sadadd3  14195  smumullem  14226  pcmpt2  14496  prmreclem4  14521  prmreclem5  14522  prmreclem6  14523  1arith  14529  ressval  14770  acsfn  15148  gsumzsplitOLD  17144  mplcoe3  18323  mplcoe3OLD  18324  mplcoe5  18326  mplcoe2OLD  18328  ordtbaslem  19856  pnfnei  19888  mnfnei  19889  uzrest  20564  fclsval  20675  blin  21090  blin2  21098  stdbdxmet  21184  nrginvrcnlem  21365  qtopbaslem  21431  metnrmlem1a  21528  metnrmlem1  21529  addcnlem  21534  evth  21625  xlebnum  21631  minveclem3b  22009  ovolicc1  22093  ismbfd  22213  mbfposr  22225  mbfi1fseqlem4  22291  mbfi1fseqlem5  22292  mbfi1flimlem  22295  itg2const  22313  itg2const2  22314  itg2splitlem  22321  itg2monolem3  22325  itg2gt0  22333  itg2cnlem1  22334  itg2cnlem2  22335  itg2cn  22336  iblre  22366  itgreval  22369  itgneg  22376  iblss  22377  itgitg1  22381  itgle  22382  itgeqa  22386  itgss3  22387  itgless  22389  iblconst  22390  itgconst  22391  ibladdlem  22392  itgaddlem2  22396  iblabslem  22400  iblabsr  22402  iblmulc2  22403  itgmulc2lem2  22405  itgsplit  22408  dveflem  22546  elply2  22759  ply1term  22767  plyeq0lem  22773  plypf1  22775  coe1termlem  22821  coe1term  22822  aalioulem5  22898  aalioulem6  22899  cxpcn3lem  23289  o1cxp  23502  cxp2lim  23504  cxploglim  23505  cxploglim2  23506  ftalem1  23544  ftalem2  23545  ftalem4  23547  muf  23612  chtdif  23630  ppidif  23635  prmorcht  23650  muinv  23667  chtppilim  23858  rplogsumlem2  23868  dchrvmasumiflem1  23884  dchrvmasumiflem2  23885  rpvmasum2  23895  rplogsum  23910  ostth2lem2  24017  ostth2lem3  24018  ostth2lem4  24019  eupath2  25182  resvval  28052  signspval  28773  signswmnd  28778  mblfinlem2  30292  mbfposadd  30302  cnambfre  30303  itg2addnclem  30306  itg2addnc  30309  itg2gt0cn  30310  ibladdnclem  30311  itgaddnclem2  30314  iblabsnclem  30318  iblmulc2nc  30320  itgmulc2nclem2  30322  bddiblnc  30325  ftc1anclem5  30334  ftc1anclem7  30336  ftc1anclem8  30337  areaquad  31425  mullimc  31861  mullimcf  31868  addlimc  31893  limclner  31896  stoweidlem5  32026  linc0scn0  33278  linc1  33280
  Copyright terms: Public domain W3C validator