Theorem ifcl 4080

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-if 4037

This theorem is referenced by:  ifcld  4081  ifpr  4180  suppr  8260  infpr  8292  ttukeylem3  9216  canthp1lem2  9354  xrmaxlt  11886  xrltmin  11887  xrmaxle  11888  xrlemin  11889  lemaxle  11900  z2ge  11903  ixxin  12063  uzsup  12524  expmulnbnd  12858  discr1  12862  uzin2  13932  rexanre  13934  caubnd  13946  limsupbnd2  14062  rlimcn2  14169  reccn2  14175  lo1mul  14206  rlimno1  14232  fsumsplit  14318  isumless  14416  explecnv  14436  cvgrat  14454  fprodsplit  14535  rpnnen2lem2  14783  sadadd2lem2  15010  sadcaddlem  15017  sadadd2lem  15019  sadadd3  15021  smumullem  15052  pcmpt2  15435  prmreclem4  15461  prmreclem5  15462  prmreclem6  15463  1arith  15469  ressval  15754  acsfn  16143  mplcoe3  19287  mplcoe5  19289  ordtbaslem  20802  pnfnei  20834  mnfnei  20835  uzrest  21511  fclsval  21622  blin  22036  blin2  22044  stdbdxmet  22130  nrginvrcnlem  22305  qtopbaslem  22372  metnrmlem1a  22469  metnrmlem1  22470  addcnlem  22475  evth  22566  xlebnum  22572  minveclem3b  23007  ovolicc1  23091  ismbfd  23213  mbfposr  23225  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1flimlem  23295  itg2const  23313  itg2const2  23314  itg2splitlem  23321  itg2monolem3  23325  itg2gt0  23333  itg2cnlem1  23334  itg2cnlem2  23335  itg2cn  23336  iblre  23366  itgreval  23369  itgneg  23376  iblss  23377  itgitg1  23381  itgle  23382  itgeqa  23386  itgss3  23387  itgless  23389  iblconst  23390  itgconst  23391  ibladdlem  23392  itgaddlem2  23396  iblabslem  23400  iblabsr  23402  iblmulc2  23403  itgmulc2lem2  23405  itgsplit  23408  dveflem  23546  elply2  23756  ply1term  23764  plyeq0lem  23770  plypf1  23772  coe1termlem  23818  coe1term  23819  aalioulem5  23895  aalioulem6  23896  cxpcn3lem  24288  o1cxp  24501  cxp2lim  24503  cxploglim  24504  cxploglim2  24505  ftalem1  24599  ftalem2  24600  ftalem4  24602  muf  24666  chtdif  24684  ppidif  24689  prmorcht  24704  muinv  24719  chtppilim  24964  rplogsumlem2  24974  dchrvmasumiflem1  24990  dchrvmasumiflem2  24991  rpvmasum2  25001  rplogsum  25016  ostth2lem2  25123  ostth2lem3  25124  ostth2lem4  25125  eupath2  26507  resvval  29158  signspval  29955  signswmnd  29960  mblfinlem2  32617  mbfposadd  32627  cnambfre  32628  itg2addnclem  32631  itg2addnc  32634  itg2gt0cn  32635  ibladdnclem  32636  itgaddnclem2  32639  iblabsnclem  32643  iblmulc2nc  32645  itgmulc2nclem2  32647  bddiblnc  32650  ftc1anclem5  32659  ftc1anclem7  32661  ftc1anclem8  32662  areaquad  36821  mullimc  38683  mullimcf  38690  addlimc  38715  limclner  38718  stoweidlem5  38898  eupth2lems  41406  linc0scn0  42006  linc1  42008