Theorem ifcl 4512

Description: Membership (closure) of a conditional operator. (Contributed by NM, 4-Apr-2005.)

Assertion

Ref	Expression
ifcl	⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)

Proof of Theorem ifcl

Step	Hyp	Ref	Expression
1		eleq1 2824	. 2 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
2		eleq1 2824	. 2 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
3	1, 2	ifboth 4506	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  ifcld  4513  ifcli  4514  ifpr  4637  suppr  9385  infpr  9418  ttukeylem3  10433  canthp1lem2  10576  xrmaxlt  13133  xrltmin  13134  xrmaxle  13135  xrlemin  13136  lemaxle  13147  z2ge  13150  ixxin  13315  uzsup  13822  expmulnbnd  14197  discr1  14201  uzin2  15307  rexanre  15309  caubnd  15321  limsupbnd2  15445  rlimcn3  15552  reccn2  15559  lo1mul  15590  rlimno1  15616  fsumsplit  15703  isumless  15810  explecnv  15830  cvgrat  15848  fprodsplit  15931  rpnnen2lem2  16182  sadadd2lem2  16419  sadcaddlem  16426  sadadd2lem  16428  sadadd3  16430  smumullem  16461  pcmpt2  16864  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  1arith  16898  ressval  17203  acsfn  17625  mplcoe3  22016  mplcoe5  22018  ordtbaslem  23153  pnfnei  23185  mnfnei  23186  uzrest  23862  fclsval  23973  blin  24386  blin2  24394  stdbdxmet  24480  nrginvrcnlem  24656  qtopbaslem  24723  metnrmlem1a  24824  metnrmlem1  24825  addcnlem  24830  evth  24926  xlebnum  24932  minveclem3b  25395  ovolicc1  25483  ismbfd  25606  mbfposr  25619  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mbfi1flimlem  25689  itg2const  25707  itg2const2  25708  itg2splitlem  25715  itg2monolem3  25719  itg2gt0  25727  itg2cnlem1  25728  itg2cnlem2  25729  itg2cn  25730  iblre  25761  itgreval  25764  itgneg  25771  iblss  25772  itgitg1  25776  itgle  25777  itgeqa  25781  itgss3  25782  itgless  25784  iblconst  25785  itgconst  25786  ibladdlem  25787  itgaddlem2  25791  iblabslem  25795  iblabsr  25797  iblmulc2  25798  itgmulc2lem2  25800  itgsplit  25803  bddiblnc  25809  dveflem  25946  elply2  26161  ply1term  26169  plyeq0lem  26175  plypf1  26177  coe1termlem  26223  coe1term  26224  aalioulem5  26302  aalioulem6  26303  cxpcn3lem  26711  o1cxp  26938  cxp2lim  26940  cxploglim  26941  cxploglim2  26942  ftalem1  27036  ftalem2  27037  ftalem4  27039  muf  27103  chtdif  27121  ppidif  27126  prmorcht  27141  muinv  27156  chtppilim  27438  rplogsumlem2  27448  dchrvmasumiflem1  27464  dchrvmasumiflem2  27465  rpvmasum2  27475  rplogsum  27490  ostth2lem2  27597  ostth2lem3  27598  ostth2lem4  27599  eupth2lems  30308  resvval  33389  signspval  34696  signswmnd  34701  mblfinlem2  37979  mbfposadd  37988  cnambfre  37989  itg2addnclem  37992  itg2addnc  37995  itg2gt0cn  37996  ibladdnclem  37997  itgaddnclem2  38000  iblabsnclem  38004  iblmulc2nc  38006  itgmulc2nclem2  38008  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anclem8  38021  areaquad  43644  mullimc  46046  mullimcf  46053  addlimc  46076  limclner  46079  stoweidlem5  46433  prproropf1olem2  47964  linc0scn0  48899  linc1  48901