Theorem ifcl 4531

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-if 4486

This theorem is used by:  ifcld  4532  ifcli  4533  ifpr  4657  suppr  9446  infpr  9479  ttukeylem3  10517  canthp1lem2  10666  xrmaxlt  13237  xrltmin  13238  xrmaxle  13239  xrlemin  13240  lemaxle  13251  z2ge  13254  ixxin  13419  uzsup  13928  expmulnbnd  14303  discr1  14307  uzin2  15436  rexanre  15438  caubnd  15450  limsupbnd2  15574  rlimcn3  15681  reccn2  15688  lo1mul  15719  rlimno1  15745  fsumsplit  15831  isumless  15938  explecnv  15958  cvgrat  15976  fprodsplit  16059  rpnnen2lem2  16309  sadadd2lem2  16546  sadcaddlem  16553  sadadd2lem  16555  sadadd3  16557  smumullem  16588  pcmpt2  16991  prmreclem4  17017  prmreclem5  17018  prmreclem6  17019  1arith  17025  ressval  17331  acsfn  17753  mplcoe3  22260  mplcoe5  22262  ordtbaslem  23419  pnfnei  23451  mnfnei  23452  uzrest  24129  fclsval  24240  blin  24653  blin2  24661  stdbdxmet  24747  nrginvrcnlem  24923  qtopbaslem  24990  metnrmlem1a  25091  metnrmlem1  25092  addcnlem  25097  evth  25193  xlebnum  25199  minveclem3b  25662  ovolicc1  25750  ismbfd  25873  mbfposr  25886  mbfi1fseqlem4  25952  mbfi1fseqlem5  25953  mbfi1flimlem  25956  itg2const  25974  itg2const2  25975  itg2splitlem  25982  itg2monolem3  25986  itg2gt0  25994  itg2cnlem1  25995  itg2cnlem2  25996  itg2cn  25997  iblre  26028  itgreval  26031  itgneg  26038  iblss  26039  itgitg1  26043  itgle  26044  itgeqa  26048  itgss3  26049  itgless  26051  iblconst  26052  itgconst  26053  ibladdlem  26054  itgaddlem2  26058  iblabslem  26062  iblabsr  26064  iblmulc2  26065  itgmulc2lem2  26067  itgsplit  26070  bddiblnc  26076  dveflem  26213  elply2  26428  ply1term  26436  plyeq0lem  26443  plypf1  26445  coe1termlem  26491  coe1term  26492  aalioulem5  26579  aalioulem6  26580  cxpcn3lem  26992  o1cxp  27219  cxp2lim  27221  cxploglim  27222  cxploglim2  27223  ftalem1  27317  ftalem2  27318  ftalem4  27320  muf  27384  chtdif  27402  ppidif  27407  prmorcht  27422  muinv  27437  chtppilim  27719  rplogsumlem2  27729  dchrvmasumiflem1  27745  dchrvmasumiflem2  27746  rpvmasum2  27756  rplogsum  27771  ostth2lem2  27878  ostth2lem3  27879  ostth2lem4  27880  eupth2lems  30726  resvval  33777  signspval  35068  signswmnd  35073  mblfinlem2  38415  mbfposadd  38424  cnambfre  38425  itg2addnclem  38428  itg2addnc  38431  itg2gt0cn  38432  ibladdnclem  38433  itgaddnclem2  38436  iblabsnclem  38440  iblmulc2nc  38442  itgmulc2nclem2  38444  ftc1anclem5  38454  ftc1anclem7  38456  ftc1anclem8  38457  areaquad  44065  mullimc  46454  mullimcf  46461  addlimc  46484  limclner  46487  stoweidlem5  46841  prproropf1olem2  48412  linc0scn0  49361  linc1  49363