Theorem ifcl 4534

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ifcif 4488

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  ifcld  4535  ifcli  4536  ifpr  4657  suppr  9423  infpr  9456  ttukeylem3  10464  canthp1lem2  10606  xrmaxlt  13141  xrltmin  13142  xrmaxle  13143  xrlemin  13144  lemaxle  13155  z2ge  13158  ixxin  13323  uzsup  13825  expmulnbnd  14200  discr1  14204  uzin2  15311  rexanre  15313  caubnd  15325  limsupbnd2  15449  rlimcn3  15556  reccn2  15563  lo1mul  15594  rlimno1  15620  fsumsplit  15707  isumless  15811  explecnv  15831  cvgrat  15849  fprodsplit  15932  rpnnen2lem2  16183  sadadd2lem2  16420  sadcaddlem  16427  sadadd2lem  16429  sadadd3  16431  smumullem  16462  pcmpt2  16864  prmreclem4  16890  prmreclem5  16891  prmreclem6  16892  1arith  16898  ressval  17203  acsfn  17620  mplcoe3  21945  mplcoe5  21947  ordtbaslem  23075  pnfnei  23107  mnfnei  23108  uzrest  23784  fclsval  23895  blin  24309  blin2  24317  stdbdxmet  24403  nrginvrcnlem  24579  qtopbaslem  24646  metnrmlem1a  24747  metnrmlem1  24748  addcnlem  24753  evth  24858  xlebnum  24864  minveclem3b  25328  ovolicc1  25417  ismbfd  25540  mbfposr  25553  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1flimlem  25623  itg2const  25641  itg2const2  25642  itg2splitlem  25649  itg2monolem3  25653  itg2gt0  25661  itg2cnlem1  25662  itg2cnlem2  25663  itg2cn  25664  iblre  25695  itgreval  25698  itgneg  25705  iblss  25706  itgitg1  25710  itgle  25711  itgeqa  25715  itgss3  25716  itgless  25718  iblconst  25719  itgconst  25720  ibladdlem  25721  itgaddlem2  25725  iblabslem  25729  iblabsr  25731  iblmulc2  25732  itgmulc2lem2  25734  itgsplit  25737  bddiblnc  25743  dveflem  25883  elply2  26101  ply1term  26109  plyeq0lem  26115  plypf1  26117  coe1termlem  26163  coe1term  26164  aalioulem5  26244  aalioulem6  26245  cxpcn3lem  26657  o1cxp  26885  cxp2lim  26887  cxploglim  26888  cxploglim2  26889  ftalem1  26983  ftalem2  26984  ftalem4  26986  muf  27050  chtdif  27068  ppidif  27073  prmorcht  27088  muinv  27103  chtppilim  27386  rplogsumlem2  27396  dchrvmasumiflem1  27412  dchrvmasumiflem2  27413  rpvmasum2  27423  rplogsum  27438  ostth2lem2  27545  ostth2lem3  27546  ostth2lem4  27547  eupth2lems  30167  resvval  33301  signspval  34543  signswmnd  34548  mblfinlem2  37652  mbfposadd  37661  cnambfre  37662  itg2addnclem  37665  itg2addnc  37668  itg2gt0cn  37669  ibladdnclem  37670  itgaddnclem2  37673  iblabsnclem  37677  iblmulc2nc  37679  itgmulc2nclem2  37681  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anclem8  37694  areaquad  43205  mullimc  45614  mullimcf  45621  addlimc  45646  limclner  45649  stoweidlem5  46003  prproropf1olem2  47505  linc0scn0  48412  linc1  48414