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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ifcif 4467

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  ifcld  4514  ifcli  4515  ifpr  4638  suppr  9378  infpr  9411  ttukeylem3  10424  canthp1lem2  10567  xrmaxlt  13124  xrltmin  13125  xrmaxle  13126  xrlemin  13127  lemaxle  13138  z2ge  13141  ixxin  13306  uzsup  13813  expmulnbnd  14188  discr1  14192  uzin2  15298  rexanre  15300  caubnd  15312  limsupbnd2  15436  rlimcn3  15543  reccn2  15550  lo1mul  15581  rlimno1  15607  fsumsplit  15694  isumless  15801  explecnv  15821  cvgrat  15839  fprodsplit  15922  rpnnen2lem2  16173  sadadd2lem2  16410  sadcaddlem  16417  sadadd2lem  16419  sadadd3  16421  smumullem  16452  pcmpt2  16855  prmreclem4  16881  prmreclem5  16882  prmreclem6  16883  1arith  16889  ressval  17194  acsfn  17616  mplcoe3  22026  mplcoe5  22028  ordtbaslem  23163  pnfnei  23195  mnfnei  23196  uzrest  23872  fclsval  23983  blin  24396  blin2  24404  stdbdxmet  24490  nrginvrcnlem  24666  qtopbaslem  24733  metnrmlem1a  24834  metnrmlem1  24835  addcnlem  24840  evth  24936  xlebnum  24942  minveclem3b  25405  ovolicc1  25493  ismbfd  25616  mbfposr  25629  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  mbfi1flimlem  25699  itg2const  25717  itg2const2  25718  itg2splitlem  25725  itg2monolem3  25729  itg2gt0  25737  itg2cnlem1  25738  itg2cnlem2  25739  itg2cn  25740  iblre  25771  itgreval  25774  itgneg  25781  iblss  25782  itgitg1  25786  itgle  25787  itgeqa  25791  itgss3  25792  itgless  25794  iblconst  25795  itgconst  25796  ibladdlem  25797  itgaddlem2  25801  iblabslem  25805  iblabsr  25807  iblmulc2  25808  itgmulc2lem2  25810  itgsplit  25813  bddiblnc  25819  dveflem  25956  elply2  26171  ply1term  26179  plyeq0lem  26185  plypf1  26187  coe1termlem  26233  coe1term  26234  aalioulem5  26313  aalioulem6  26314  cxpcn3lem  26724  o1cxp  26952  cxp2lim  26954  cxploglim  26955  cxploglim2  26956  ftalem1  27050  ftalem2  27051  ftalem4  27053  muf  27117  chtdif  27135  ppidif  27140  prmorcht  27155  muinv  27170  chtppilim  27452  rplogsumlem2  27462  dchrvmasumiflem1  27478  dchrvmasumiflem2  27479  rpvmasum2  27489  rplogsum  27504  ostth2lem2  27611  ostth2lem3  27612  ostth2lem4  27613  eupth2lems  30323  resvval  33404  signspval  34712  signswmnd  34717  mblfinlem2  37993  mbfposadd  38002  cnambfre  38003  itg2addnclem  38006  itg2addnc  38009  itg2gt0cn  38010  ibladdnclem  38011  itgaddnclem2  38014  iblabsnclem  38018  iblmulc2nc  38020  itgmulc2nclem2  38022  ftc1anclem5  38032  ftc1anclem7  38034  ftc1anclem8  38035  areaquad  43662  mullimc  46064  mullimcf  46071  addlimc  46094  limclner  46097  stoweidlem5  46451  prproropf1olem2  47976  linc0scn0  48911  linc1  48913