Theorem ifcl 4507

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-if 4462

This theorem is referenced by:  ifcld  4508  ifcli  4509  ifpr  4632  suppr  9382  infpr  9415  ttukeylem3  10431  canthp1lem2  10574  xrmaxlt  13131  xrltmin  13132  xrmaxle  13133  xrlemin  13134  lemaxle  13145  z2ge  13148  ixxin  13313  uzsup  13820  expmulnbnd  14195  discr1  14199  uzin2  15305  rexanre  15307  caubnd  15319  limsupbnd2  15443  rlimcn3  15550  reccn2  15557  lo1mul  15588  rlimno1  15614  fsumsplit  15701  isumless  15808  explecnv  15828  cvgrat  15846  fprodsplit  15929  rpnnen2lem2  16180  sadadd2lem2  16417  sadcaddlem  16424  sadadd2lem  16426  sadadd3  16428  smumullem  16459  pcmpt2  16862  prmreclem4  16888  prmreclem5  16889  prmreclem6  16890  1arith  16896  ressval  17201  acsfn  17623  mplcoe3  22021  mplcoe5  22023  ordtbaslem  23178  pnfnei  23210  mnfnei  23211  uzrest  23887  fclsval  23998  blin  24411  blin2  24419  stdbdxmet  24505  nrginvrcnlem  24681  qtopbaslem  24748  metnrmlem1a  24849  metnrmlem1  24850  addcnlem  24855  evth  24951  xlebnum  24957  minveclem3b  25420  ovolicc1  25508  ismbfd  25631  mbfposr  25644  mbfi1fseqlem4  25710  mbfi1fseqlem5  25711  mbfi1flimlem  25714  itg2const  25732  itg2const2  25733  itg2splitlem  25740  itg2monolem3  25744  itg2gt0  25752  itg2cnlem1  25753  itg2cnlem2  25754  itg2cn  25755  iblre  25786  itgreval  25789  itgneg  25796  iblss  25797  itgitg1  25801  itgle  25802  itgeqa  25806  itgss3  25807  itgless  25809  iblconst  25810  itgconst  25811  ibladdlem  25812  itgaddlem2  25816  iblabslem  25820  iblabsr  25822  iblmulc2  25823  itgmulc2lem2  25825  itgsplit  25828  bddiblnc  25834  dveflem  25971  elply2  26186  ply1term  26194  plyeq0lem  26200  plypf1  26202  coe1termlem  26248  coe1term  26249  aalioulem5  26327  aalioulem6  26328  cxpcn3lem  26736  o1cxp  26963  cxp2lim  26965  cxploglim  26966  cxploglim2  26967  ftalem1  27061  ftalem2  27062  ftalem4  27064  muf  27128  chtdif  27146  ppidif  27151  prmorcht  27166  muinv  27181  chtppilim  27463  rplogsumlem2  27473  dchrvmasumiflem1  27489  dchrvmasumiflem2  27490  rpvmasum2  27500  rplogsum  27515  ostth2lem2  27622  ostth2lem3  27623  ostth2lem4  27624  eupth2lems  30333  resvval  33419  signspval  34743  signswmnd  34748  mblfinlem2  38032  mbfposadd  38041  cnambfre  38042  itg2addnclem  38045  itg2addnc  38048  itg2gt0cn  38049  ibladdnclem  38050  itgaddnclem2  38053  iblabsnclem  38057  iblmulc2nc  38059  itgmulc2nclem2  38061  ftc1anclem5  38071  ftc1anclem7  38073  ftc1anclem8  38074  areaquad  43668  mullimc  46068  mullimcf  46075  addlimc  46098  limclner  46101  stoweidlem5  46455  prproropf1olem2  47986  linc0scn0  48921  linc1  48923