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

Theorem ifcl 3896
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 2494 . 2  |-  ( A  =  if ( ph ,  A ,  B )  ->  ( A  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
2 eleq1 2494 . 2  |-  ( B  =  if ( ph ,  A ,  B )  ->  ( B  e.  C  <->  if ( ph ,  A ,  B )  e.  C ) )
31, 2ifboth 3890 1  |-  ( ( A  e.  C  /\  B  e.  C )  ->  if ( ph ,  A ,  B )  e.  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    e. wcel 1872   ifcif 3854
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-if 3855
This theorem is referenced by:  ifcld  3897  ifpr  3991  suppr  7940  infpr  7972  ttukeylem3  8892  canthp1lem2  9029  xrmaxlt  11427  xrltmin  11428  xrmaxle  11429  xrlemin  11430  z2ge  11442  ixxin  11603  uzsup  12040  expmulnbnd  12354  discr1  12358  uzin2  13351  rexanre  13353  caubnd  13365  limsupbnd2  13489  limsupbnd2OLD  13490  rlimcn2  13597  reccn2  13603  lo1mul  13634  rlimno1  13660  fsumsplit  13749  isumless  13846  explecnv  13866  cvgrat  13882  fprodsplit  13963  rpnnen2lem2  14211  sadadd2lem2  14367  sadcaddlem  14374  sadadd2lem  14376  sadadd3  14378  smumullem  14409  pcmpt2  14781  prmreclem4  14806  prmreclem5  14807  prmreclem6  14808  1arith  14814  ressval  15119  acsfn  15508  mplcoe3  18633  mplcoe5  18635  ordtbaslem  20146  pnfnei  20178  mnfnei  20179  uzrest  20854  fclsval  20965  blin  21378  blin2  21386  stdbdxmet  21472  nrginvrcnlem  21635  qtopbaslem  21721  metnrmlem1a  21817  metnrmlem1  21818  metnrmlem1aOLD  21832  metnrmlem1OLD  21833  addcnlem  21838  evth  21929  xlebnum  21938  minveclem3b  22312  minveclem3bOLD  22324  ovolicc1  22411  ismbfd  22538  mbfposr  22550  mbfi1fseqlem4  22618  mbfi1fseqlem5  22619  mbfi1flimlem  22622  itg2const  22640  itg2const2  22641  itg2splitlem  22648  itg2monolem3  22652  itg2gt0  22660  itg2cnlem1  22661  itg2cnlem2  22662  itg2cn  22663  iblre  22693  itgreval  22696  itgneg  22703  iblss  22704  itgitg1  22708  itgle  22709  itgeqa  22713  itgss3  22714  itgless  22716  iblconst  22717  itgconst  22718  ibladdlem  22719  itgaddlem2  22723  iblabslem  22727  iblabsr  22729  iblmulc2  22730  itgmulc2lem2  22732  itgsplit  22735  dveflem  22873  elply2  23092  ply1term  23100  plyeq0lem  23106  plypf1  23108  coe1termlem  23154  coe1term  23155  aalioulem5  23234  aalioulem6  23235  cxpcn3lem  23629  o1cxp  23842  cxp2lim  23844  cxploglim  23845  cxploglim2  23846  ftalem1  23939  ftalem2  23940  ftalem4  23942  ftalem4OLD  23944  muf  24009  chtdif  24027  ppidif  24032  prmorcht  24047  muinv  24064  chtppilim  24255  rplogsumlem2  24265  dchrvmasumiflem1  24281  dchrvmasumiflem2  24282  rpvmasum2  24292  rplogsum  24307  ostth2lem2  24414  ostth2lem3  24415  ostth2lem4  24416  eupath2  25650  resvval  28542  signspval  29393  signswmnd  29398  mblfinlem2  31885  mbfposadd  31895  cnambfre  31896  itg2addnclem  31900  itg2addnc  31903  itg2gt0cn  31904  ibladdnclem  31905  itgaddnclem2  31908  iblabsnclem  31912  iblmulc2nc  31914  itgmulc2nclem2  31916  bddiblnc  31919  ftc1anclem5  31928  ftc1anclem7  31930  ftc1anclem8  31931  areaquad  36014  mullimc  37579  mullimcf  37586  addlimc  37612  limclner  37615  stoweidlem5  37748  linc0scn0  39819  linc1  39821
  Copyright terms: Public domain W3C validator