Theorem ifcl 4566

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2098  ifcif 4521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-if 4522

This theorem is referenced by:  ifcld  4567  ifcli  4568  ifpr  4688  suppr  9463  infpr  9495  ttukeylem3  10503  canthp1lem2  10645  xrmaxlt  13158  xrltmin  13159  xrmaxle  13160  xrlemin  13161  lemaxle  13172  z2ge  13175  ixxin  13339  uzsup  13826  expmulnbnd  14196  discr1  14200  uzin2  15289  rexanre  15291  caubnd  15303  limsupbnd2  15425  rlimcn3  15532  reccn2  15539  lo1mul  15570  rlimno1  15598  fsumsplit  15685  isumless  15789  explecnv  15809  cvgrat  15827  fprodsplit  15908  rpnnen2lem2  16157  sadadd2lem2  16390  sadcaddlem  16397  sadadd2lem  16399  sadadd3  16401  smumullem  16432  pcmpt2  16827  prmreclem4  16853  prmreclem5  16854  prmreclem6  16855  1arith  16861  ressval  17177  acsfn  17604  mplcoe3  21905  mplcoe5  21907  ordtbaslem  23016  pnfnei  23048  mnfnei  23049  uzrest  23725  fclsval  23836  blin  24251  blin2  24259  stdbdxmet  24348  nrginvrcnlem  24532  qtopbaslem  24599  metnrmlem1a  24698  metnrmlem1  24699  addcnlem  24704  evth  24809  xlebnum  24815  minveclem3b  25280  ovolicc1  25369  ismbfd  25492  mbfposr  25505  mbfi1fseqlem4  25572  mbfi1fseqlem5  25573  mbfi1flimlem  25576  itg2const  25594  itg2const2  25595  itg2splitlem  25602  itg2monolem3  25606  itg2gt0  25614  itg2cnlem1  25615  itg2cnlem2  25616  itg2cn  25617  iblre  25647  itgreval  25650  itgneg  25657  iblss  25658  itgitg1  25662  itgle  25663  itgeqa  25667  itgss3  25668  itgless  25670  iblconst  25671  itgconst  25672  ibladdlem  25673  itgaddlem2  25677  iblabslem  25681  iblabsr  25683  iblmulc2  25684  itgmulc2lem2  25686  itgsplit  25689  bddiblnc  25695  dveflem  25835  elply2  26052  ply1term  26060  plyeq0lem  26066  plypf1  26068  coe1termlem  26114  coe1term  26115  aalioulem5  26192  aalioulem6  26193  cxpcn3lem  26601  o1cxp  26826  cxp2lim  26828  cxploglim  26829  cxploglim2  26830  ftalem1  26924  ftalem2  26925  ftalem4  26927  muf  26991  chtdif  27009  ppidif  27014  prmorcht  27029  muinv  27044  chtppilim  27327  rplogsumlem2  27337  dchrvmasumiflem1  27353  dchrvmasumiflem2  27354  rpvmasum2  27364  rplogsum  27379  ostth2lem2  27486  ostth2lem3  27487  ostth2lem4  27488  eupth2lems  29963  resvval  32910  signspval  34055  signswmnd  34060  mblfinlem2  37020  mbfposadd  37029  cnambfre  37030  itg2addnclem  37033  itg2addnc  37036  itg2gt0cn  37037  ibladdnclem  37038  itgaddnclem2  37041  iblabsnclem  37045  iblmulc2nc  37047  itgmulc2nclem2  37049  ftc1anclem5  37059  ftc1anclem7  37061  ftc1anclem8  37062  areaquad  42479  mullimc  44842  mullimcf  44849  addlimc  44874  limclner  44877  stoweidlem5  45231  prproropf1olem2  46682  linc0scn0  47317  linc1  47319