Theorem ifcl 4574

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 2822	. 2 ⊢ (𝐴 = if(𝜑, 𝐴, 𝐵) → (𝐴 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
2		eleq1 2822	. 2 ⊢ (𝐵 = if(𝜑, 𝐴, 𝐵) → (𝐵 ∈ 𝐶 ↔ if(𝜑, 𝐴, 𝐵) ∈ 𝐶))
3	1, 2	ifboth 4568	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  ifcld  4575  ifcli  4576  ifpr  4696  suppr  9466  infpr  9498  ttukeylem3  10506  canthp1lem2  10648  xrmaxlt  13160  xrltmin  13161  xrmaxle  13162  xrlemin  13163  lemaxle  13174  z2ge  13177  ixxin  13341  uzsup  13828  expmulnbnd  14198  discr1  14202  uzin2  15291  rexanre  15293  caubnd  15305  limsupbnd2  15427  rlimcn3  15534  reccn2  15541  lo1mul  15572  rlimno1  15600  fsumsplit  15687  isumless  15791  explecnv  15811  cvgrat  15829  fprodsplit  15910  rpnnen2lem2  16158  sadadd2lem2  16391  sadcaddlem  16398  sadadd2lem  16400  sadadd3  16402  smumullem  16433  pcmpt2  16826  prmreclem4  16852  prmreclem5  16853  prmreclem6  16854  1arith  16860  ressval  17176  acsfn  17603  mplcoe3  21593  mplcoe5  21595  ordtbaslem  22692  pnfnei  22724  mnfnei  22725  uzrest  23401  fclsval  23512  blin  23927  blin2  23935  stdbdxmet  24024  nrginvrcnlem  24208  qtopbaslem  24275  metnrmlem1a  24374  metnrmlem1  24375  addcnlem  24380  evth  24475  xlebnum  24481  minveclem3b  24945  ovolicc1  25033  ismbfd  25156  mbfposr  25169  mbfi1fseqlem4  25236  mbfi1fseqlem5  25237  mbfi1flimlem  25240  itg2const  25258  itg2const2  25259  itg2splitlem  25266  itg2monolem3  25270  itg2gt0  25278  itg2cnlem1  25279  itg2cnlem2  25280  itg2cn  25281  iblre  25311  itgreval  25314  itgneg  25321  iblss  25322  itgitg1  25326  itgle  25327  itgeqa  25331  itgss3  25332  itgless  25334  iblconst  25335  itgconst  25336  ibladdlem  25337  itgaddlem2  25341  iblabslem  25345  iblabsr  25347  iblmulc2  25348  itgmulc2lem2  25350  itgsplit  25353  bddiblnc  25359  dveflem  25496  elply2  25710  ply1term  25718  plyeq0lem  25724  plypf1  25726  coe1termlem  25772  coe1term  25773  aalioulem5  25849  aalioulem6  25850  cxpcn3lem  26255  o1cxp  26479  cxp2lim  26481  cxploglim  26482  cxploglim2  26483  ftalem1  26577  ftalem2  26578  ftalem4  26580  muf  26644  chtdif  26662  ppidif  26667  prmorcht  26682  muinv  26697  chtppilim  26978  rplogsumlem2  26988  dchrvmasumiflem1  27004  dchrvmasumiflem2  27005  rpvmasum2  27015  rplogsum  27030  ostth2lem2  27137  ostth2lem3  27138  ostth2lem4  27139  eupth2lems  29491  resvval  32441  signspval  33563  signswmnd  33568  mblfinlem2  36526  mbfposadd  36535  cnambfre  36536  itg2addnclem  36539  itg2addnc  36542  itg2gt0cn  36543  ibladdnclem  36544  itgaddnclem2  36547  iblabsnclem  36551  iblmulc2nc  36553  itgmulc2nclem2  36555  ftc1anclem5  36565  ftc1anclem7  36567  ftc1anclem8  36568  areaquad  41965  mullimc  44332  mullimcf  44339  addlimc  44364  limclner  44367  stoweidlem5  44721  prproropf1olem2  46172  linc0scn0  47104  linc1  47106