Theorem ifcl 4130

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

Step	Hyp	Ref	Expression
1		eleq1 2689	. 2 |- ( A = if ( ph , A , B ) -> ( A e. C <-> if ( ph , A , B ) e. C ) )
2		eleq1 2689	. 2 |- ( B = if ( ph , A , B ) -> ( B e. C <-> if ( ph , A , B ) e. C ) )
3	1, 2	ifboth 4124	1 |- ( ( A e. C /\ B e. C ) -> if ( ph , A , B ) e. C )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   ifcif 4086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-if 4087

This theorem is referenced by:  ifcld  4131  ifpr  4233  suppr  8377  infpr  8409  ttukeylem3  9333  canthp1lem2  9475  xrmaxlt  12012  xrltmin  12013  xrmaxle  12014  xrlemin  12015  lemaxle  12026  z2ge  12029  ixxin  12192  uzsup  12662  expmulnbnd  12996  discr1  13000  uzin2  14084  rexanre  14086  caubnd  14098  limsupbnd2  14214  rlimcn2  14321  reccn2  14327  lo1mul  14358  rlimno1  14384  fsumsplit  14471  isumless  14577  explecnv  14597  cvgrat  14615  fprodsplit  14696  rpnnen2lem2  14944  sadadd2lem2  15172  sadcaddlem  15179  sadadd2lem  15181  sadadd3  15183  smumullem  15214  pcmpt2  15597  prmreclem4  15623  prmreclem5  15624  prmreclem6  15625  1arith  15631  ressval  15927  acsfn  16320  mplcoe3  19466  mplcoe5  19468  ordtbaslem  20992  pnfnei  21024  mnfnei  21025  uzrest  21701  fclsval  21812  blin  22226  blin2  22234  stdbdxmet  22320  nrginvrcnlem  22495  qtopbaslem  22562  metnrmlem1a  22661  metnrmlem1  22662  addcnlem  22667  evth  22758  xlebnum  22764  minveclem3b  23199  ovolicc1  23284  ismbfd  23407  mbfposr  23419  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfi1flimlem  23489  itg2const  23507  itg2const2  23508  itg2splitlem  23515  itg2monolem3  23519  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  itg2cn  23530  iblre  23560  itgreval  23563  itgneg  23570  iblss  23571  itgitg1  23575  itgle  23576  itgeqa  23580  itgss3  23581  itgless  23583  iblconst  23584  itgconst  23585  ibladdlem  23586  itgaddlem2  23590  iblabslem  23594  iblabsr  23596  iblmulc2  23597  itgmulc2lem2  23599  itgsplit  23602  dveflem  23742  elply2  23952  ply1term  23960  plyeq0lem  23966  plypf1  23968  coe1termlem  24014  coe1term  24015  aalioulem5  24091  aalioulem6  24092  cxpcn3lem  24488  o1cxp  24701  cxp2lim  24703  cxploglim  24704  cxploglim2  24705  ftalem1  24799  ftalem2  24800  ftalem4  24802  muf  24866  chtdif  24884  ppidif  24889  prmorcht  24904  muinv  24919  chtppilim  25164  rplogsumlem2  25174  dchrvmasumiflem1  25190  dchrvmasumiflem2  25191  rpvmasum2  25201  rplogsum  25216  ostth2lem2  25323  ostth2lem3  25324  ostth2lem4  25325  eupth2lems  27098  resvval  29827  signspval  30629  signswmnd  30634  mblfinlem2  33447  mbfposadd  33457  cnambfre  33458  itg2addnclem  33461  itg2addnc  33464  itg2gt0cn  33465  ibladdnclem  33466  itgaddnclem2  33469  iblabsnclem  33473  iblmulc2nc  33475  itgmulc2nclem2  33477  bddiblnc  33480  ftc1anclem5  33489  ftc1anclem7  33491  ftc1anclem8  33492  areaquad  37802  mullimc  39848  mullimcf  39855  addlimc  39880  limclner  39883  stoweidlem5  40222  linc0scn0  42212  linc1  42214