Theorem ifcl 4521

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ifcif 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-if 4476

This theorem is referenced by:  ifcld  4522  ifcli  4523  ifpr  4646  suppr  9356  infpr  9389  ttukeylem3  10402  canthp1lem2  10544  xrmaxlt  13080  xrltmin  13081  xrmaxle  13082  xrlemin  13083  lemaxle  13094  z2ge  13097  ixxin  13262  uzsup  13767  expmulnbnd  14142  discr1  14146  uzin2  15252  rexanre  15254  caubnd  15266  limsupbnd2  15390  rlimcn3  15497  reccn2  15504  lo1mul  15535  rlimno1  15561  fsumsplit  15648  isumless  15752  explecnv  15772  cvgrat  15790  fprodsplit  15873  rpnnen2lem2  16124  sadadd2lem2  16361  sadcaddlem  16368  sadadd2lem  16370  sadadd3  16372  smumullem  16403  pcmpt2  16805  prmreclem4  16831  prmreclem5  16832  prmreclem6  16833  1arith  16839  ressval  17144  acsfn  17565  mplcoe3  21974  mplcoe5  21976  ordtbaslem  23104  pnfnei  23136  mnfnei  23137  uzrest  23813  fclsval  23924  blin  24337  blin2  24345  stdbdxmet  24431  nrginvrcnlem  24607  qtopbaslem  24674  metnrmlem1a  24775  metnrmlem1  24776  addcnlem  24781  evth  24886  xlebnum  24892  minveclem3b  25356  ovolicc1  25445  ismbfd  25568  mbfposr  25581  mbfi1fseqlem4  25647  mbfi1fseqlem5  25648  mbfi1flimlem  25651  itg2const  25669  itg2const2  25670  itg2splitlem  25677  itg2monolem3  25681  itg2gt0  25689  itg2cnlem1  25690  itg2cnlem2  25691  itg2cn  25692  iblre  25723  itgreval  25726  itgneg  25733  iblss  25734  itgitg1  25738  itgle  25739  itgeqa  25743  itgss3  25744  itgless  25746  iblconst  25747  itgconst  25748  ibladdlem  25749  itgaddlem2  25753  iblabslem  25757  iblabsr  25759  iblmulc2  25760  itgmulc2lem2  25762  itgsplit  25765  bddiblnc  25771  dveflem  25911  elply2  26129  ply1term  26137  plyeq0lem  26143  plypf1  26145  coe1termlem  26191  coe1term  26192  aalioulem5  26272  aalioulem6  26273  cxpcn3lem  26685  o1cxp  26913  cxp2lim  26915  cxploglim  26916  cxploglim2  26917  ftalem1  27011  ftalem2  27012  ftalem4  27014  muf  27078  chtdif  27096  ppidif  27101  prmorcht  27116  muinv  27131  chtppilim  27414  rplogsumlem2  27424  dchrvmasumiflem1  27440  dchrvmasumiflem2  27441  rpvmasum2  27451  rplogsum  27466  ostth2lem2  27573  ostth2lem3  27574  ostth2lem4  27575  eupth2lems  30216  resvval  33292  signspval  34563  signswmnd  34568  mblfinlem2  37704  mbfposadd  37713  cnambfre  37714  itg2addnclem  37717  itg2addnc  37720  itg2gt0cn  37721  ibladdnclem  37722  itgaddnclem2  37725  iblabsnclem  37729  iblmulc2nc  37731  itgmulc2nclem2  37733  ftc1anclem5  37743  ftc1anclem7  37745  ftc1anclem8  37746  areaquad  43255  mullimc  45662  mullimcf  45669  addlimc  45692  limclner  45695  stoweidlem5  46049  prproropf1olem2  47541  linc0scn0  48461  linc1  48463