Theorem ifcl 4468

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2111  ifcif 4423

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-if 4424

This theorem is referenced by:  ifcld  4469  ifcli  4470  ifpr  4589  suppr  8973  infpr  9005  ttukeylem3  9976  canthp1lem2  10118  xrmaxlt  12620  xrltmin  12621  xrmaxle  12622  xrlemin  12623  lemaxle  12634  z2ge  12637  ixxin  12801  uzsup  13285  expmulnbnd  13651  discr1  13655  uzin2  14757  rexanre  14759  caubnd  14771  limsupbnd2  14893  rlimcn2  15000  reccn2  15006  lo1mul  15037  rlimno1  15063  fsumsplit  15150  isumless  15253  explecnv  15273  cvgrat  15292  fprodsplit  15373  rpnnen2lem2  15621  sadadd2lem2  15854  sadcaddlem  15861  sadadd2lem  15863  sadadd3  15865  smumullem  15896  pcmpt2  16289  prmreclem4  16315  prmreclem5  16316  prmreclem6  16317  1arith  16323  ressval  16614  acsfn  16993  mplcoe3  20803  mplcoe5  20805  ordtbaslem  21893  pnfnei  21925  mnfnei  21926  uzrest  22602  fclsval  22713  blin  23128  blin2  23136  stdbdxmet  23222  nrginvrcnlem  23398  qtopbaslem  23465  metnrmlem1a  23564  metnrmlem1  23565  addcnlem  23570  evth  23665  xlebnum  23671  minveclem3b  24133  ovolicc1  24221  ismbfd  24344  mbfposr  24357  mbfi1fseqlem4  24423  mbfi1fseqlem5  24424  mbfi1flimlem  24427  itg2const  24445  itg2const2  24446  itg2splitlem  24453  itg2monolem3  24457  itg2gt0  24465  itg2cnlem1  24466  itg2cnlem2  24467  itg2cn  24468  iblre  24498  itgreval  24501  itgneg  24508  iblss  24509  itgitg1  24513  itgle  24514  itgeqa  24518  itgss3  24519  itgless  24521  iblconst  24522  itgconst  24523  ibladdlem  24524  itgaddlem2  24528  iblabslem  24532  iblabsr  24534  iblmulc2  24535  itgmulc2lem2  24537  itgsplit  24540  bddiblnc  24546  dveflem  24683  elply2  24897  ply1term  24905  plyeq0lem  24911  plypf1  24913  coe1termlem  24959  coe1term  24960  aalioulem5  25036  aalioulem6  25037  cxpcn3lem  25440  o1cxp  25664  cxp2lim  25666  cxploglim  25667  cxploglim2  25668  ftalem1  25762  ftalem2  25763  ftalem4  25765  muf  25829  chtdif  25847  ppidif  25852  prmorcht  25867  muinv  25882  chtppilim  26163  rplogsumlem2  26173  dchrvmasumiflem1  26189  dchrvmasumiflem2  26190  rpvmasum2  26200  rplogsum  26215  ostth2lem2  26322  ostth2lem3  26323  ostth2lem4  26324  eupth2lems  28127  resvval  31056  signspval  32054  signswmnd  32059  mblfinlem2  35401  mbfposadd  35410  cnambfre  35411  itg2addnclem  35414  itg2addnc  35417  itg2gt0cn  35418  ibladdnclem  35419  itgaddnclem2  35422  iblabsnclem  35426  iblmulc2nc  35428  itgmulc2nclem2  35430  ftc1anclem5  35440  ftc1anclem7  35442  ftc1anclem8  35443  areaquad  40567  mullimc  42652  mullimcf  42659  addlimc  42684  limclner  42687  stoweidlem5  43041  prproropf1olem2  44417  linc0scn0  45225  linc1  45227