Theorem ifcl 4546

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 4540	1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → if(𝜑, 𝐴, 𝐵) ∈ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ifcif 4500

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  ifcld  4547  ifcli  4548  ifpr  4669  suppr  9482  infpr  9515  ttukeylem3  10523  canthp1lem2  10665  xrmaxlt  13195  xrltmin  13196  xrmaxle  13197  xrlemin  13198  lemaxle  13209  z2ge  13212  ixxin  13377  uzsup  13878  expmulnbnd  14251  discr1  14255  uzin2  15361  rexanre  15363  caubnd  15375  limsupbnd2  15497  rlimcn3  15604  reccn2  15611  lo1mul  15642  rlimno1  15668  fsumsplit  15755  isumless  15859  explecnv  15879  cvgrat  15897  fprodsplit  15980  rpnnen2lem2  16231  sadadd2lem2  16467  sadcaddlem  16474  sadadd2lem  16476  sadadd3  16478  smumullem  16509  pcmpt2  16911  prmreclem4  16937  prmreclem5  16938  prmreclem6  16939  1arith  16945  ressval  17252  acsfn  17669  mplcoe3  21994  mplcoe5  21996  ordtbaslem  23124  pnfnei  23156  mnfnei  23157  uzrest  23833  fclsval  23944  blin  24358  blin2  24366  stdbdxmet  24452  nrginvrcnlem  24628  qtopbaslem  24695  metnrmlem1a  24796  metnrmlem1  24797  addcnlem  24802  evth  24907  xlebnum  24913  minveclem3b  25378  ovolicc1  25467  ismbfd  25590  mbfposr  25603  mbfi1fseqlem4  25669  mbfi1fseqlem5  25670  mbfi1flimlem  25673  itg2const  25691  itg2const2  25692  itg2splitlem  25699  itg2monolem3  25703  itg2gt0  25711  itg2cnlem1  25712  itg2cnlem2  25713  itg2cn  25714  iblre  25745  itgreval  25748  itgneg  25755  iblss  25756  itgitg1  25760  itgle  25761  itgeqa  25765  itgss3  25766  itgless  25768  iblconst  25769  itgconst  25770  ibladdlem  25771  itgaddlem2  25775  iblabslem  25779  iblabsr  25781  iblmulc2  25782  itgmulc2lem2  25784  itgsplit  25787  bddiblnc  25793  dveflem  25933  elply2  26151  ply1term  26159  plyeq0lem  26165  plypf1  26167  coe1termlem  26213  coe1term  26214  aalioulem5  26294  aalioulem6  26295  cxpcn3lem  26707  o1cxp  26935  cxp2lim  26937  cxploglim  26938  cxploglim2  26939  ftalem1  27033  ftalem2  27034  ftalem4  27036  muf  27100  chtdif  27118  ppidif  27123  prmorcht  27138  muinv  27153  chtppilim  27436  rplogsumlem2  27446  dchrvmasumiflem1  27462  dchrvmasumiflem2  27463  rpvmasum2  27473  rplogsum  27488  ostth2lem2  27595  ostth2lem3  27596  ostth2lem4  27597  eupth2lems  30165  resvval  33291  signspval  34530  signswmnd  34535  mblfinlem2  37628  mbfposadd  37637  cnambfre  37638  itg2addnclem  37641  itg2addnc  37644  itg2gt0cn  37645  ibladdnclem  37646  itgaddnclem2  37649  iblabsnclem  37653  iblmulc2nc  37655  itgmulc2nclem2  37657  ftc1anclem5  37667  ftc1anclem7  37669  ftc1anclem8  37670  areaquad  43187  mullimc  45593  mullimcf  45600  addlimc  45625  limclner  45628  stoweidlem5  45982  prproropf1olem2  47466  linc0scn0  48347  linc1  48349