Theorem ifcl 4573

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ifcif 4528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4529

This theorem is referenced by:  ifcld  4574  ifcli  4575  ifpr  4695  suppr  9463  infpr  9495  ttukeylem3  10503  canthp1lem2  10645  xrmaxlt  13157  xrltmin  13158  xrmaxle  13159  xrlemin  13160  lemaxle  13171  z2ge  13174  ixxin  13338  uzsup  13825  expmulnbnd  14195  discr1  14199  uzin2  15288  rexanre  15290  caubnd  15302  limsupbnd2  15424  rlimcn3  15531  reccn2  15538  lo1mul  15569  rlimno1  15597  fsumsplit  15684  isumless  15788  explecnv  15808  cvgrat  15826  fprodsplit  15907  rpnnen2lem2  16155  sadadd2lem2  16388  sadcaddlem  16395  sadadd2lem  16397  sadadd3  16399  smumullem  16430  pcmpt2  16823  prmreclem4  16849  prmreclem5  16850  prmreclem6  16851  1arith  16857  ressval  17173  acsfn  17600  mplcoe3  21585  mplcoe5  21587  ordtbaslem  22684  pnfnei  22716  mnfnei  22717  uzrest  23393  fclsval  23504  blin  23919  blin2  23927  stdbdxmet  24016  nrginvrcnlem  24200  qtopbaslem  24267  metnrmlem1a  24366  metnrmlem1  24367  addcnlem  24372  evth  24467  xlebnum  24473  minveclem3b  24937  ovolicc1  25025  ismbfd  25148  mbfposr  25161  mbfi1fseqlem4  25228  mbfi1fseqlem5  25229  mbfi1flimlem  25232  itg2const  25250  itg2const2  25251  itg2splitlem  25258  itg2monolem3  25262  itg2gt0  25270  itg2cnlem1  25271  itg2cnlem2  25272  itg2cn  25273  iblre  25303  itgreval  25306  itgneg  25313  iblss  25314  itgitg1  25318  itgle  25319  itgeqa  25323  itgss3  25324  itgless  25326  iblconst  25327  itgconst  25328  ibladdlem  25329  itgaddlem2  25333  iblabslem  25337  iblabsr  25339  iblmulc2  25340  itgmulc2lem2  25342  itgsplit  25345  bddiblnc  25351  dveflem  25488  elply2  25702  ply1term  25710  plyeq0lem  25716  plypf1  25718  coe1termlem  25764  coe1term  25765  aalioulem5  25841  aalioulem6  25842  cxpcn3lem  26245  o1cxp  26469  cxp2lim  26471  cxploglim  26472  cxploglim2  26473  ftalem1  26567  ftalem2  26568  ftalem4  26570  muf  26634  chtdif  26652  ppidif  26657  prmorcht  26672  muinv  26687  chtppilim  26968  rplogsumlem2  26978  dchrvmasumiflem1  26994  dchrvmasumiflem2  26995  rpvmasum2  27005  rplogsum  27020  ostth2lem2  27127  ostth2lem3  27128  ostth2lem4  27129  eupth2lems  29481  resvval  32430  signspval  33552  signswmnd  33557  mblfinlem2  36515  mbfposadd  36524  cnambfre  36525  itg2addnclem  36528  itg2addnc  36531  itg2gt0cn  36532  ibladdnclem  36533  itgaddnclem2  36536  iblabsnclem  36540  iblmulc2nc  36542  itgmulc2nclem2  36544  ftc1anclem5  36554  ftc1anclem7  36556  ftc1anclem8  36557  areaquad  41951  mullimc  44319  mullimcf  44326  addlimc  44351  limclner  44354  stoweidlem5  44708  prproropf1olem2  46159  linc0scn0  47058  linc1  47060