Theorem ifcl 4510

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2104  ifcif 4465

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-if 4466

This theorem is referenced by:  ifcld  4511  ifcli  4512  ifpr  4631  suppr  9274  infpr  9306  ttukeylem3  10313  canthp1lem2  10455  xrmaxlt  12961  xrltmin  12962  xrmaxle  12963  xrlemin  12964  lemaxle  12975  z2ge  12978  ixxin  13142  uzsup  13629  expmulnbnd  13996  discr1  14000  uzin2  15101  rexanre  15103  caubnd  15115  limsupbnd2  15237  rlimcn3  15344  reccn2  15351  lo1mul  15382  rlimno1  15410  fsumsplit  15498  isumless  15602  explecnv  15622  cvgrat  15640  fprodsplit  15721  rpnnen2lem2  15969  sadadd2lem2  16202  sadcaddlem  16209  sadadd2lem  16211  sadadd3  16213  smumullem  16244  pcmpt2  16639  prmreclem4  16665  prmreclem5  16666  prmreclem6  16667  1arith  16673  ressval  16989  acsfn  17413  mplcoe3  21284  mplcoe5  21286  ordtbaslem  22384  pnfnei  22416  mnfnei  22417  uzrest  23093  fclsval  23204  blin  23619  blin2  23627  stdbdxmet  23716  nrginvrcnlem  23900  qtopbaslem  23967  metnrmlem1a  24066  metnrmlem1  24067  addcnlem  24072  evth  24167  xlebnum  24173  minveclem3b  24637  ovolicc1  24725  ismbfd  24848  mbfposr  24861  mbfi1fseqlem4  24928  mbfi1fseqlem5  24929  mbfi1flimlem  24932  itg2const  24950  itg2const2  24951  itg2splitlem  24958  itg2monolem3  24962  itg2gt0  24970  itg2cnlem1  24971  itg2cnlem2  24972  itg2cn  24973  iblre  25003  itgreval  25006  itgneg  25013  iblss  25014  itgitg1  25018  itgle  25019  itgeqa  25023  itgss3  25024  itgless  25026  iblconst  25027  itgconst  25028  ibladdlem  25029  itgaddlem2  25033  iblabslem  25037  iblabsr  25039  iblmulc2  25040  itgmulc2lem2  25042  itgsplit  25045  bddiblnc  25051  dveflem  25188  elply2  25402  ply1term  25410  plyeq0lem  25416  plypf1  25418  coe1termlem  25464  coe1term  25465  aalioulem5  25541  aalioulem6  25542  cxpcn3lem  25945  o1cxp  26169  cxp2lim  26171  cxploglim  26172  cxploglim2  26173  ftalem1  26267  ftalem2  26268  ftalem4  26270  muf  26334  chtdif  26352  ppidif  26357  prmorcht  26372  muinv  26387  chtppilim  26668  rplogsumlem2  26678  dchrvmasumiflem1  26694  dchrvmasumiflem2  26695  rpvmasum2  26705  rplogsum  26720  ostth2lem2  26827  ostth2lem3  26828  ostth2lem4  26829  eupth2lems  28647  resvval  31571  signspval  32576  signswmnd  32581  mblfinlem2  35859  mbfposadd  35868  cnambfre  35869  itg2addnclem  35872  itg2addnc  35875  itg2gt0cn  35876  ibladdnclem  35877  itgaddnclem2  35880  iblabsnclem  35884  iblmulc2nc  35886  itgmulc2nclem2  35888  ftc1anclem5  35898  ftc1anclem7  35900  ftc1anclem8  35901  areaquad  41085  mullimc  43206  mullimcf  43213  addlimc  43238  limclner  43241  stoweidlem5  43595  prproropf1olem2  45014  linc0scn0  45822  linc1  45824