Theorem ifcl 4513

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114  ifcif 4469

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-if 4470

This theorem is referenced by:  ifcld  4514  ifcli  4515  ifexg  4516  ifpr  4631  suppr  8937  infpr  8969  ttukeylem3  9935  canthp1lem2  10077  xrmaxlt  12577  xrltmin  12578  xrmaxle  12579  xrlemin  12580  lemaxle  12591  z2ge  12594  ixxin  12758  uzsup  13234  expmulnbnd  13599  discr1  13603  uzin2  14706  rexanre  14708  caubnd  14720  limsupbnd2  14842  rlimcn2  14949  reccn2  14955  lo1mul  14986  rlimno1  15012  fsumsplit  15099  isumless  15202  explecnv  15222  cvgrat  15241  fprodsplit  15322  rpnnen2lem2  15570  sadadd2lem2  15801  sadcaddlem  15808  sadadd2lem  15810  sadadd3  15812  smumullem  15843  pcmpt2  16231  prmreclem4  16257  prmreclem5  16258  prmreclem6  16259  1arith  16265  ressval  16553  acsfn  16932  mplcoe3  20249  mplcoe5  20251  ordtbaslem  21798  pnfnei  21830  mnfnei  21831  uzrest  22507  fclsval  22618  blin  23033  blin2  23041  stdbdxmet  23127  nrginvrcnlem  23302  qtopbaslem  23369  metnrmlem1a  23468  metnrmlem1  23469  addcnlem  23474  evth  23565  xlebnum  23571  minveclem3b  24033  ovolicc1  24119  ismbfd  24242  mbfposr  24255  mbfi1fseqlem4  24321  mbfi1fseqlem5  24322  mbfi1flimlem  24325  itg2const  24343  itg2const2  24344  itg2splitlem  24351  itg2monolem3  24355  itg2gt0  24363  itg2cnlem1  24364  itg2cnlem2  24365  itg2cn  24366  iblre  24396  itgreval  24399  itgneg  24406  iblss  24407  itgitg1  24411  itgle  24412  itgeqa  24416  itgss3  24417  itgless  24419  iblconst  24420  itgconst  24421  ibladdlem  24422  itgaddlem2  24426  iblabslem  24430  iblabsr  24432  iblmulc2  24433  itgmulc2lem2  24435  itgsplit  24438  dveflem  24578  elply2  24788  ply1term  24796  plyeq0lem  24802  plypf1  24804  coe1termlem  24850  coe1term  24851  aalioulem5  24927  aalioulem6  24928  cxpcn3lem  25330  o1cxp  25554  cxp2lim  25556  cxploglim  25557  cxploglim2  25558  ftalem1  25652  ftalem2  25653  ftalem4  25655  muf  25719  chtdif  25737  ppidif  25742  prmorcht  25757  muinv  25772  chtppilim  26053  rplogsumlem2  26063  dchrvmasumiflem1  26079  dchrvmasumiflem2  26080  rpvmasum2  26090  rplogsum  26105  ostth2lem2  26212  ostth2lem3  26213  ostth2lem4  26214  eupth2lems  28019  resvval  30902  signspval  31824  signswmnd  31829  mblfinlem2  34932  mbfposadd  34941  cnambfre  34942  itg2addnclem  34945  itg2addnc  34948  itg2gt0cn  34949  ibladdnclem  34950  itgaddnclem2  34953  iblabsnclem  34957  iblmulc2nc  34959  itgmulc2nclem2  34961  bddiblnc  34964  ftc1anclem5  34973  ftc1anclem7  34975  ftc1anclem8  34976  areaquad  39830  mullimc  41904  mullimcf  41911  addlimc  41936  limclner  41939  stoweidlem5  42297  prproropf1olem2  43673  linc0scn0  44485  linc1  44487